eqt>

Theorem.

Arguments:

(obj), (obj), (obj),

Assertions:

(()(()()))

Proof:

Hyp	Ref	Line	Expr
	ax-tr	1	(()(()()))
1	com12i	2	(()(()()))
	ax-tr	3	(()(()()))
3	com12i	4	(()(()()))
2, 4	im.bldan<>	5	((()())((()())(()())))
	df-equ	6	(()(()()))
	dfbi	7	((()())((()())(()())))
5, 6, 7	<imtr	8	(()(()()))