case all _ _ _ ih =>
  rw [CutRestricted.cast, CutRestricted.all', CutRestricted.cast]
  exact ih _; simp
L : Language
Δ✝¹ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → SyntacticTerm L), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ : Sequent L
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
ih : ∀ (f : ℕ → SyntacticTerm L), CutRestricted C a✝ → CutRestricted C (Derivation.rewrite a✝ f)
f : ℕ → SyntacticTerm L
⊢ CutRestricted C a✝ →
    CutRestricted C
      (Derivation.cast (Derivation.all (Derivation.cast (Derivation.rewrite a✝ (&0 :>ₙ fun x => ⇑ (f x))) ⋯)) ⋯)
no goals