Description: Existential Instantiation. Virtual Deduction rule corresponding to a
special case of the Natural Deduction Sequent Calculus rule called Rule
C in Margaris p. 79 and E E. in Table 1 on page 4 of the paper
"Extracting information from intermediate T-systems" (2000) presented at
IMLA99 by Mauro Ferrari, Camillo Fiorentini, and Pierangelo Miglioli.
(Contributed by Alan Sare, 21-Apr-2013)(Proof modification is discouraged.)(New usage is discouraged.)