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