cbvex

Theorem.

Arguments:

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

Hypotheses:

(()())

( bound in )

( bound in )

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(()())
		2	( bound in )
		3	( bound in )
3	bv-¬	4	( bound in )
2	bv-¬	5	( bound in )
1	bi.bldnegd	6	(()())
4, 5, 6	cbval	7	()
7	bi.bldneg	8	()
	df-ex	9	()
	df-ex	10	()
8, 9, 10	<2bitr	11	()