existential instantiation <2023-09-21 Thu 23:45:26> mahmood math a rule of inference: where is a new constant symbol that has not appeared in the proof.