Classically known as Existential Instantiation, this rule allows you to infer a claim from an existential generalization if you can derive it from the assumption of a genuinely arbitrary instance of that generalization.
Preview shown for the Point And Click derivation type in the LRC_O system