simp [varSumInR, Matrix.vecAppend_eq_ite]
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
no goals