df<-alt2

Theorem.

Arguments:

(obj), (obj),

Assertions:

(()(()()))

Proof:

Hyp	Ref	Line	Expr
	df-psub	1	(()(()()))
	df-neq	2	(()())
2	bi.bldan>	3	((()())(()()))
1, 3	bitr	4	(()(()()))