simp[CutFree, CutRestricted.lMap]
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
no goals