imgen<i

Theorem.

Arguments:

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

Hypotheses:

()

( bound in )

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	()
		2	( bound in )
1	im.bldex	3	()
2	fv.eqex	4	()
3, 4	brpi22<	5	()