Existential Instantiation
This video presents the same text shown beside it, spoken and on screen. It adds nothing the text does not say.
State
From (∃x)Fx, derive Fa — where a is a name new to the proof.
Show
Something did it; call it a. But a must be a fresh name, carrying no prior commitments.
Watch for
The strictest restriction in the system. Reusing an existing name quietly asserts that two somethings are the same something.