imgen>i

Theorem.

Arguments:

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

Hypotheses:

()

( bound in )

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	()
		2	( bound in )
1	ax-gen	3	()
2	imgen>	4	(()())
3, 4	bmp>	5	()