eqsex

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Hypotheses:

(()())

( bound in )

Assertions:

((()))

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(()())
		2	( bound in )
	exn.al	3	((())(()))
	df-an	4	((())(()))
4	eqt-∃-i	5	((())(()))
2	bv-¬	6	( bound in )
1	bi.bldnegd	7	(()())
6, 7	eqsal	8	((()))
8	conb>i	9	((()))
3, 5, 9	<2bitr	10	((()))