Axiom 12 for predicate logic: If x is some fixed a and p(x) holds,
then for all x which are equal to a, p(x) holds. This expresses the
substitution property of =, but the name shadowing on x allows us to
express this without changing p,
because we haven't defined proper substitution yet.
axiom ax_12 {x: nat} (a: nat) (p: wff x): $ x = a -> p -> A. x (x = a -> p) $;