Theorem: LO.FirstOrder.Derivation.CutFree.lMap (Logic/FirstOrder/Basic/Calculus.lean)

State before:
L : Language
Δ✝ Δ₁✝ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
L₁ : Language
L₂ : Language
Δ₁ Γ₁ : Finset (SyntacticFormula L₁)
Δ : Sequent L₁
Φ : L₁ →ᵥ L₂
d :  ⊢¹ Δ
⊢ CutFree (Derivation.lMap Φ d) ↔ CutFree d
Tactic:
simp[CutFree, CutRestricted.lMap]
State after:
no goals