induction d <;> simp[Derivation.lMap, *]
L : Language
Δ✝ Δ₁✝ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
L₁ : Language
L₂ : Language
Δ₁ Γ₁ : Finset (SyntacticFormula L₁)
C : Set (SyntacticFormula L₂)
Δ : Sequent L₁
Φ : L₁ →ᵥ L₂
d :  ⊢¹ Δ
⊢ CutRestricted C (Derivation.lMap Φ d) ↔ CutRestricted (⇑(Semiformula.lMap Φ) ⁻¹' C) d
no goals