sylan>
Theorem.
Arguments:
(pr),
(pr),
(pr),
(pr),
Hypotheses:
(
)
((
)
)
Assertions:
((
)
)
Proof:
Hyp
Ref
Line
Expr
Hypo
1
(
)
2
((
)
)
2
exp
3
(
(
))
1, 3
rpi32
4
(
(
))
4
imp
5
((
)
)