Axiom 5 for predicate logic: If p does not contain an occurrence of x
(note that (p: wff) in contrast to (p: wff x) means that p cannot
depend on variable x), then p implies A. x p
because the quantifier is trivial.
axiom ax_5 {x: nat} (p: wff): $ p -> A. x p $;