Axiom ax_11 | index | src |

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 $;