alor<

Theorem.

Arguments:

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

Hypotheses:

( bound in )

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	( bound in )
1	bv-¬	2	( bound in )
2	imgen>	3	(()())
	df-or	4	(()())
4	eqt-∀-i	5	(()())
	df-or	6	(()())
3, 5, 6	<2bitr	7	(()())