Axiom ax_4 | index | src |

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