rintro ⟨⟩
L : Language
Δ✝ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
d :  ⊢¹ Δ
ss : Δ ⊆ Γ
⊢ CutRestricted C (Derivation.wk d ss) → CutRestricted C d
case wk
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ✝ Γ : Sequent L
p q : SyntacticFormula L
d :  ⊢¹ Δ✝
ss : Δ✝ ⊆ Γ
Δ : Sequent L
ss✝ : Δ✝ ⊆ Γ
a✝ : CutRestricted C d
⊢ CutRestricted C d