Theorem: vac_contra (Lectures/NatRec.lean)

State before:
⊢ ∀ (e : Empty) (n : ℕ), wrong n = e → n = 2
Tactic:
intro e
State after:
e : Empty
⊢ ∀ (n : ℕ), wrong n = e → n = 2

State before:
e : Empty
⊢ ∀ (n : ℕ), wrong n = e → n = 2
Tactic:
induction e
State after:
no goals