Theorem: LO.FirstOrder.Semiterm.substs_varSumInL (Logic/FirstOrder/Basic/Eq.lean)

State before:
L : Language
μ : Type u_1
inst✝ : Semiformula.Operator.Eq L
k n : ℕ
w₁ w₂ : Fin k → Semiterm L μ n
i : Fin k
⊢ (Rew.substs (Matrix.vecAppend ⋯ w₁ w₂)) (varSumInL i) = w₁ i
Tactic:
simp [varSumInL, Matrix.vecAppend_eq_ite]
State after:
no goals