assumption
case cut.left
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ✝
dn :  ⊢¹ ~p :: Δ✝
Δ : Sequent L
a✝² : p ∈ C
a✝¹ : CutRestricted C dp
a✝ : CutRestricted C dn
⊢ p ∈ C
no goals