rintro ⟨⟩
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p✝ q : SyntacticFormula L
p : Semiformula L ℕ (0 + 1)
d :  ⊢¹ (Rew.hom Rew.free) p :: Δ⁺
⊢ CutRestricted C (Derivation.all d) → CutRestricted C d
case all
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p✝ q : SyntacticFormula L
p : Semiformula L ℕ (0 + 1)
d :  ⊢¹ (Rew.hom Rew.free) p :: Δ✝⁺
Δ : Sequent L
a✝ : CutRestricted C d
⊢ CutRestricted C d