sb-eqat<x

Theorem.

Arguments:

(sv), (sv),

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ),

Assertions:

[/]()

Proof:

Hyp	Ref	Line	Expr
	eqid	1	()
1	eqvini-sv	2	(()())
	eqcomi	3	(()())
3	im.bldan<	4	((()())(()()))
2, 4	im.bldex	5	(()())
	eqvini-sv	6	(()(()()))
	eqcomi	7	(()())
7	im.bldan<	8	((()())(()()))
6, 8	im.bldex	9	(()(()()))
9	im.bldan>	10	((()())(()(()())))
5, 10	im.bldex	11	(()(()()))
11	df-sb	12	[/]()