Universal quantifier introduction rule
= Universal quantifier introduction rule
If $A(u)$ is proved and $u$ is not free in any undischarged assumption, infer $\forall x\,A(x)$, with capture-free replacement. The freshness condition prevents generalizing from a special object.