Theorem: LO.FirstOrder.shifts_emb (Logic/FirstOrder/Basic/Calculus.lean)

State before:
L : Language
n : ℕ
Γ : List (Semisentence L n)
⊢ (List.map (⇑Rew.emb.hom) Γ)⁺ = List.map (⇑Rew.emb.hom) Γ
Tactic:
simp[shifts, Function.comp, ←Rew.hom_comp_app]
State after:
no goals