eqt-sb

Theorem.

Arguments:

(st), (st), (sv), (pr),

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ), (, ), (, ),

Assertions:

(()([/][/]))

Proof:

Hyp	Ref	Line	Expr
	eqt>	1	(()(()()))
	ax17-bv	2	( bound in ())
1	bi.bldan<d	3	(()((()(()))(()(()))))
2, 3	bi.bldexd	4	(()((()(()))(()(()))))
	df-sb	5	([/](()(())))
	df-sb	6	([/](()(())))
4, 5, 6	<2bitrg	7	(()([/][/]))