sbal-w

Theorem.

Arguments:

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

Distinct variable conditions:

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

Assertions:

([/][/])

Proof:

Hyp	Ref	Line	Expr
	ax17-bv	1	( bound in ())
1	imgen>	2	((())(()))
2	eqt-∀-i	3	((())(()))
	alcom	4	((())(()))
3, 4	bitr	5	((())(()))
	dfsb-dval	6	([/](()))
	dfsb-dval	7	([/](()))
7	eqt-∀-i	8	([/](()))
5, 6, 8	<2bitr	9	([/][/])
9	bicomi	10	([/][/])