Axiom ax_gen | index | src |

The axiom of generalization. If |- p is derivable (the lack of a precondition means this is a proof in the empty context), then p is universally true, so |- A. x p is also true.

axiom ax_gen {x: nat} (p: wff x): $ p $ > $ A. x p $;