case all => rw[length_cast] <;> simp[Rew.q_rewrite, *]
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
Δ✝ : List (SyntacticSemiformula L 0)
p✝ : Semiformula L ℕ (0 + 1)
a✝ : Derivation ((Rew.hom Rew.free) p✝ :: Δ✝⁺)
a_ih✝ : ∀ (f : ℕ → SyntacticTerm L), length (rewrite a✝ f) = length a✝
f : ℕ → SyntacticTerm L
⊢ length (Derivation.cast (all (Derivation.cast (rewrite a✝ (&0 :>ₙ fun x => ⇑ (f x))) ⋯)) ⋯) = length a✝ + 1
no goals