case wk _ _ _ _ ih => exact ih
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝¹ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ Γ✝ : Sequent L
a✝¹ : Derivation Δ✝
a✝ : Δ✝ ⊆ Γ✝
ih : CutRestricted C a✝¹ → CutRestricted C' a✝¹
⊢ CutRestricted C a✝¹ → CutRestricted C' a✝¹
no goals