Theorem: Matrix.eq_vecCons' (Arithmetization/Vorspiel/Vorspiel.lean)

State before:
n : ℕ
C : Type u_1
s : Fin (n + 1) → C
⊢ (s 0 :> fun x => s x.succ) 0 = s 0
Tactic:
simp
State after:
no goals

State before:
n : ℕ
C : Type u_1
s : Fin (n + 1) → C
⊢ ∀ (i : Fin n), (s 0 :> fun x => s x.succ) i.succ = s i.succ
Tactic:
simp
State after:
no goals