exact ih
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✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
ih : CutRestricted C a✝ → CutRestricted C' a✝
⊢ CutRestricted C a✝ → CutRestricted C' a✝
no goals