sb-eqat<

Theorem.

Arguments:

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

Dummy variables:

(sv),

Distinct variable conditions:

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

Assertions:

([/]()())

Proof:

Hyp	Ref	Line	Expr
	ax17-bv	1	( bound in ())
	sb-eqat<w	2	([/]()())
2	bi.bldsb	3	([/][/]()[/]())
	sb-eqat<w	4	([/]()())
3, 4	bitr	5	([/][/]()())
1	sbco2	6	([/][/]()[/]())
5, 6	<>bitr	7	([/]()())