bexim

Theorem.

Arguments:

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

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	al.andi	1	(()())
	an.nim	2	(()())
2	eqt-∀-i	3	(()())
	df-an	4	(()())
1, 3, 4	>2bitr	5	(()())
5	conb>i	6	(()())
	df-ex	7	()
7	bi.bldim>	8	(()())
	df-ex	9	(()())
6, 8, 9	<2bitr<	10	(()())