no goals
α : Type u
m n o : ℕ
m' : Type ?u.14497
n' : Type ?u.14500
o' : Type ?u.14503
i : ℕ
h : Nat.succ i < Nat.succ m
x : α
u : Fin m → α
⊢ vecCons x u { val := Nat.succ i, isLt := h } = u { val := i, isLt := (_ : i < m) }
simp only [vecCons, Fin.cons, Fin.cases_succ']