exintr

Theorem.

Arguments:

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

Assertions:

(()(()))

Proof:

Hyp	Ref	Line	Expr
	bv-∀b	1	( bound in ())
	anc<	2	(()(()))
2	ax4	3	(()(()))
1, 3	im.bldexd	4	(()(()))