Existential quantifier introduction rule
= Existential quantifier introduction rule
From $A(t)$, infer $\exists x\,A(x)$ when the substitution is capture-free. The term $t$ supplies a witness.
= Existential quantifier introduction rule
From $A(t)$, infer $\exists x\,A(x)$ when the substitution is capture-free. The term $t$ supplies a witness.