 Universal quantifier introduction rule

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