exact x.elim0
case zero.e_a.h
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
β : Fin 0 → Type u
v : (i : Fin 0) → β i
x : Fin 0
⊢ finZeroElim x = v x
no goals