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

State before:
L : Language
n : ℕ
Δ Γ : List (SyntacticSemiformula L n)
⊢ (Δ ++ Γ)⁺ = Δ⁺ ++ Γ⁺
Tactic:
simp[shifts]
State after:
no goals