Theorem: Matrix.vecCons_zero (Logic/Vorspiel/Vorspiel.lean)

State before:
n : ℕ
α : Type u
α✝ : Type u_1
a : α✝
n✝ : ℕ
s : Fin n✝ → α✝
⊢ (a :> s) 0 = a
Tactic:
simp
State after:
no goals