sb-bvw

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Hypotheses:

( bound in )

Assertions:

([/])

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
	dfsb-dvex	2	([/](()))
1	exan>	3	((())(()))
2, 3	bitr	4	([/](()))
	ax9ex	5	()
5	an-true<	6	((()))
4, 6	><bitr	7	([/])