cbvex2

Theorem.

Arguments:

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

Distinct variable conditions:

(, ), (, ), (, ), (, ),

Hypotheses:

((()())())

( bound in )

( bound in )

( bound in )

( bound in )

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	((()())())
		2	( bound in )
		3	( bound in )
		4	( bound in )
		5	( bound in )
5	bv-∃	6	( bound in )
3	bv-∃	7	( bound in )
	ax17eq	8	( bound in ())
4, 8	bv-∧	9	( bound in (()))
	ax17eq	10	( bound in ())
2, 10	bv-∧	11	( bound in (()))
1	exp	12	(()(()()))
12	com12i	13	(()(()()))
13	im.bidian	14	(()((())(())))
9, 11, 14	cbvex	15	((())(()))
10	exan<	16	((())(()))
8	exan<	17	((())(()))
15, 16, 17	>2bitr	18	((())(()))
18	im.bidian	19	(()())
6, 7, 19	cbvex	20	()