Theorem: LO.FirstOrder.Semiterm.emb_varSumInL (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 (varSumInL i) = varSumInL i
Tactic:
simp [varSumInL]
State after:
no goals