Universal Generalization
This video presents the same text shown beside it, spoken and on screen. It adds nothing the text does not say.
State
From Fy, where y is arbitrary, derive (x)Fx. Restriction: y must not have been introduced by EI, nor be free in an undischarged assumption.
Show
Proved for an arbitrary y, with no smuggled specifics — then proved for all.
Watch for
"Arbitrary" is load-bearing. Generalizing from a name is how one proves that everything is Socrates.