sbco2w

Theorem.

Arguments:

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

Distinct variable conditions:

(, ), (, ),

Hypotheses:

( bound in )

Assertions:

([/][/][/])

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
1	dfsbf	2	([/](()(())))
	dfsb-dvex	3	([/][/](()[/]))
	dfsb-dvex	4	([/](()))
4	bi.bldan>	5	((()[/])(()(())))
5	eqt-∃-i	6	((()[/])(()(())))
3, 6	bitr	7	([/][/](()(())))
2, 7	><bitr	8	([/][/][/])