simp[shifts, shiftEmb, Finset.map_eq_image, Finset.image_image, Function.comp, Semiformula.lMap_shift]
L : Language
Δ✝ Δ₁✝ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
L₁ : Language
L₂ : Language
Δ₁ Γ₁ : Finset (SyntacticFormula L₁)
Φ : L₁ →ᵥ L₂
Δ : List (SyntacticFormula L₁)
⊢ (List.map (⇑(lMap Φ)) Δ)⁺ = List.map (⇑(lMap Φ)) Δ⁺
no goals