eqs5lem

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Assertions:

((())(()))

Proof:

Hyp	Ref	Line	Expr
	ax11	1	(()((())))
1	imp	2	((())(()))
	bv-∀b	3	( bound in (()))
2, 3	imgen<i	4	((())(()))