α : Type u
m n o : ℕ
m' : Type ?u.22403
n' : Type ?u.22406
o' : Type ?u.22409
x : α
u : Fin (Nat.succ m) → α
⊢ u 0 = vecHead u
α : Type u
m n o : ℕ
m' : Type ?u.22403
n' : Type ?u.22406
o' : Type ?u.22409
x : α
u : Fin (Nat.succ m) → α
⊢ vecCons x u 1 = vecHead u
rw [← Fin.succ_zero_eq_one, cons_val_succ]
no goals
α : Type u
m n o : ℕ
m' : Type ?u.22403
n' : Type ?u.22406
o' : Type ?u.22409
x : α
u : Fin (Nat.succ m) → α
⊢ u 0 = vecHead u
rfl