have : 0 = Fin.last 0 := by rfl
n : ℕ
α : Type u
s : Fin 0 → α
a : α
x : Fin (Nat.succ 0)
⊢ (s <: a) x = ![a] x
n : ℕ
α : Type u
s : Fin 0 → α
a : α
x : Fin (Nat.succ 0)
this : 0 = last 0
⊢ (s <: a) x = ![a] x