excomim

Theorem.

Arguments:

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

Assertions:

()

Proof:

Hyp	Ref	Line	Expr
	spec-ex	1	()
1	im.bldex	2	()
2	im.bldex	3	()
	bv-∃b	4	( bound in )
4	bv-∃	5	( bound in )
5	fv.eqex	6	()
3, 6	brpi22<	7	()