eqvin

Theorem.

Arguments:

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

Distinct variable conditions:

(, ), (, ),

Assertions:

(()(()()))

Proof:

Hyp	Ref	Line	Expr
	eqvini	1	(()(()()))
	ax17-bv	2	( bound in ())
	eqtr	3	(()(()()))
3	imp	4	((()())())
2, 4	imgen<i	5	((()())())
1, 5	>bii	6	(()(()()))