Universal quantification introduction. A universal quantification ∀x. P x is shown from hypotheses H by deriving P u from H for a parameter u that does not occur free in H and ∀x. P x. That is to say, we show that something holds for all x by parametrizing the proof over u.