sb-eqat>

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Assertions:

([/]()())

Proof:

Hyp	Ref	Line	Expr
	sb-eqat<	1	([/]()())
	com	2	(()())
2	bi.bldsb	3	([/]()[/]())
	com	4	(()())
1, 3, 4	<2bitr	5	([/]()())