Universal 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 — or Fy — for any constant or variable. What's true of everything is true of each thing.
Show
(x)(Hx ⊃ Mx), so Hs ⊃ Ms. Socrates inherits the rule.
Watch for
UI is generous — instantiate to anything. The other three quantifier rules are not so relaxed.