an.andi>

Theorem.

Arguments:

(pr), (pr), (pr),

Assertions:

((())(()()))

Proof:

Hyp	Ref	Line	Expr
	anidm	1	(())
1	bicomi	2	(())
2	bi.bldan>	3	((())(()()))
	4anass	4	((()())(()()))
3, 4	bitr	5	((())(()()))