fv-nalx

Theorem.

Arguments:

(sv), (pr),

Assertions:

( bound in )

Proof:

Hyp	Ref	Line	Expr
	bv-∀b	1	( bound in )
1	bv-¬	2	( bound in )