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.
|- p
p
|- A. x p
axiom ax_gen {x: nat} (p: wff x): $ p $ > $ A. x p $;