dfsbf

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

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

Hypotheses:

( bound in )

Assertions:

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

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
	df-sb	2	([/](()(())))
	eqt>	3	(()(()()))
3	bi.bldan<d	4	(()((())(())))
	ax17-bv	5	( bound in ())
4, 5	bi.bldexd	6	(()((())(())))
	eqt<	7	(()(()()))
6, 7	bi.bldan<>d	8	(()((()(()))(()(()))))
	ax17-bv	9	( bound in (()(())))
	ax17-bv	10	( bound in ())
	ax17-bv	11	( bound in ())
1, 11	bv-∧	12	( bound in (()))
12	bv-∃	13	( bound in (()))
10, 13	bv-∧	14	( bound in (()(())))
8, 9, 14	cbvex	15	((()(()))(()(())))
2, 15	bitr	16	([/](()(())))