eqt<>d2r
Theorem.
Arguments:
(obj),
(obj),
(obj),
(obj),
(pr),
(pr),
Hypotheses:
(
(
))
(
(
))
Assertions:
((
)
((
)
(
)))
Proof:
Hyp
Ref
Line
Expr
Hypo
1
(
(
))
2
(
(
))
1, 2
eqt<>d2
3
((
)
((
)
(
)))
3
ancom
4
((
)
((
)
(
)))