Rule. uq_elim
(H ⊢ ∀x. P x) → (H ⊢ P t)