cases' x using Fin.cases with i <;> simp[this]
n : ℕ
α : Type u
s : Fin 0 → α
a : α
x : Fin (Nat.succ 0)
this : 0 = last 0
⊢ (s <: a) x = ![a] x
case succ
n : ℕ
α : Type u
s : Fin 0 → α
a : α
this : 0 = last 0
i : Fin 0
⊢ (s <: a) i.succ = a