simp only [h]
case e
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
h : ¬i < n
⊢ a = if h : i < n then a else a
case e
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
h : ¬i < n
⊢ a = if h : False then a else a