simp only [snoc]
V : Type ?u.7787
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ snoc l x (last n) = x
V : Type ?u.7787
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ (if h : (last n).val < n then l { val := (last n).val, isLt := h } else x) = x