Stuff for data.fin.vec_notation

theorem Function.update_head {α : Type u_1} {i : ℕ} {x y : α} {t : Fin i → α} : update (Matrix.vecCons x t) 0 y = Matrix.vecCons y t

theorem Function.update_cons_one {α : Type u_1} {i : ℕ} {x y z : α} {t : Fin i → α} : update (Matrix.vecCons x (Matrix.vecCons y t)) 1 z = Matrix.vecCons x (Matrix.vecCons z t)

theorem Function.update_cons_two {α : Type u_1} {i : ℕ} {w x y z : α} {t : Fin i → α} : update (Matrix.vecCons w (Matrix.vecCons x (Matrix.vecCons y t))) 2 z = Matrix.vecCons w (Matrix.vecCons x (Matrix.vecCons z t))

theorem Function.swap_cons {α : Type u_1} {i : ℕ} {x y : α} {t : Fin i → α} : Matrix.vecCons x (Matrix.vecCons y t) ∘ ⇑(Equiv.swap 0 1) = Matrix.vecCons y (Matrix.vecCons x t)