Axiom 11 for predicate logic: forall quantifiers commute.
axiom ax_11 {x y: nat} (p: wff x y): $ A. x A. y p -> A. y A. x p $;