dfsb-alt

Theorem.

Arguments:

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

Distinct variable conditions:

(, ), (, ),

Hypotheses:

( bound in )

Assertions:

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

Proof:

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