Axiom 4 for predicate logic: forall distributes over implication.
axiom ax_4 {x: nat} (p q: wff x): $ A. x (p -> q) -> A. x p -> A. x q $;