fv-imt

Theorem.

Arguments:

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

Hypotheses:

(())

( bound in )

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(())
		2	( bound in )
1	ax2	3	(()())
2	imgen>	4	(()())
3, 4	brpi22<	5	(()())