intro h hp hn
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
ihp : CutRestricted C a✝¹ → CutRestricted C' a✝¹
ihn : CutRestricted C a✝ → CutRestricted C' a✝
⊢ p✝ ∈ C → CutRestricted C a✝¹ → CutRestricted C a✝ → p✝ ∈ C' ∧ CutRestricted C' a✝¹ ∧ CutRestricted C' a✝
L : Language
Δ✝¹ Δ₁ Δ₂ Γ✝ : Sequent L
p✝¹ q✝ r : SyntacticFormula L
C C' : Set (SyntacticFormula L)
Δ Γ : Sequent L
p q : SyntacticFormula L
ss : C ⊆ C'
Δ✝ : List (SyntacticFormula L)
p✝ : SyntacticFormula L
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
ihp : CutRestricted C a✝¹ → CutRestricted C' a✝¹
ihn : CutRestricted C a✝ → CutRestricted C' a✝
h : p✝ ∈ C
hp : CutRestricted C a✝¹
hn : CutRestricted C a✝
⊢ p✝ ∈ C' ∧ CutRestricted C' a✝¹ ∧ CutRestricted C' a✝