sb-eqat<w

Theorem.

Arguments:

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

Distinct variable conditions:

(, ), (, ),

Assertions:

([/]()())

Proof:

Hyp	Ref	Line	Expr
	ax17-bv	1	( bound in ())
	eqt<	2	(()(()()))
1, 2	sb-xplw	3	([/]()())