rintro ⟨h, dp, dq⟩
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp :  ⊢¹ p :: Δ
dn :  ⊢¹ ~p :: Δ
⊢ p ∈ C ∧ CutRestricted C dp ∧ CutRestricted C dn → CutRestricted C (Derivation.cut dp dn)
case intro.intro
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
dp✝ :  ⊢¹ p :: Δ
dn :  ⊢¹ ~p :: Δ
h : p ∈ C
dp : CutRestricted C dp✝
dq : CutRestricted C dn
⊢ CutRestricted C (Derivation.cut dp✝ dn)