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

State before:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
k : ℕ
o : Type u_2
inst✝ : IsEmpty o
i : Fin k
⊢ Rew.emb (varSumInR i) = varSumInR i
Tactic:
simp [varSumInR]
State after:
no goals