Theorem: LO.FirstOrder.Semiterm.substs_varSumInR (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₂)) (varSumInR i) = w₂ i
Tactic:
simp [varSumInR, Matrix.vecAppend_eq_ite]
State after:
no goals