 Universal quantifier elimination rule

From $\forall xA(x)$, infer $A(t)$ provided the substitution is free for $x$, meaning no free variable of $t$ becomes captured.