Axiom 10 for predicate logic: x is bound in ~(A. x p), so we can
safely introduce a A. x quantifier. (This axiom is used to internalize
the notion of "bound in" when axiom 5 does not apply.)
axiom ax_10 {x: nat} (p: wff x): $ ~A. x p -> A. x ~A. x p $;