Theorem: Empty.eq_elim (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Sort u
f : Empty → α
⊢ ∀ (x : Empty), f x = x.elim
Tactic:
rintro ⟨⟩
State after:
no goals