eqt-∃

Theorem.

Arguments:

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

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	bi>	1	(()())
1	im.bldal	2	(()())
	im.bldext	3	(()())
2, 3	syl	4	(()())
	bi<	5	(()())
5	im.bldal	6	(()())
	im.bldext	7	(()())
6, 7	syl	8	(()())
4, 8	>bid	9	(()())