Theorem: eq_finZeroElim (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Sort u
x : Fin 0 → α
⊢ ∀ (x_1 : Fin 0), x x_1 = finZeroElim x_1
Tactic:
rintro ⟨_, _⟩
State after:
case mk
α : Sort u
x : Fin 0 → α
val✝ : ℕ
isLt✝ : val✝ < 0
⊢ x ⟨val✝, isLt✝⟩ = finZeroElim ⟨val✝, isLt✝⟩

State before:
case mk
α : Sort u
x : Fin 0 → α
val✝ : ℕ
isLt✝ : val✝ < 0
⊢ x ⟨val✝, isLt✝⟩ = finZeroElim ⟨val✝, isLt✝⟩
Tactic:
contradiction
State after:
no goals