Theorem: Qq.vecCons_assoc_eq (Logic/Vorspiel/Meta.lean)

State before:
α : Type u_1
n : ℕ
t : Fin n.succ → α
a b : α
s : Fin n → α
h : s <: b = t
⊢ (a :> s) <: b = a :> t
Tactic:
simp[←h, Matrix.vecCons_assoc]
State after:
no goals