cbvald

Theorem.

Arguments:

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

Distinct variable conditions:

(, ), (, ),

Hypotheses:

((()()))

(())

( bound in )

Assertions:

(())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	((()()))
		2	(())
		3	( bound in )
2, 3	fv-imt	4	(()())
4	df-Bvp	5	( bound in ())
	ax17-bv	6	( bound in ())
1	com12i	7	(()(()))
7	im.bidi	8	(()(()()))
5, 6, 8	cbval	9	(()())
	imgen>	10	(()())
3	imgen>	11	(()())
9, 10, 11	>2bitr	12	(()())
12	im.bidi	13	(())