chvar

Theorem.

Arguments:

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

Hypotheses:

(()())

( bound in )

Assertions:

Proof:

Hyp	Ref	Line	Expr
	Hypo	1
		2	(()())
		3	( bound in )
2	bi>	4	(()())
3, 4	ax4a	5	()
1, 5	mpg	6