induction d generalizing f <;> simp[*, Derivation.rewrite, -List.map_cons]
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
d :  ⊢¹ Δ
f : ℕ → SyntacticTerm L
⊢ length (rewrite d f) = length d
case axL
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
Δ✝ : List (SyntacticFormula L)
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ℕ 0
f : ℕ → SyntacticTerm L
⊢ length (id (axL (List.map (⇑(Rew.rewrite f).hom) Δ✝) r✝ fun i => (Rew.rewrite f) (v✝ i))) = 0

case all
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

case ex
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
Δ✝ : List (SyntacticFormula L)
p✝ : Semiformula L ℕ (Nat.succ 0)
t✝ : Semiterm L ℕ 0
a✝ : Derivation ([→ t✝].hom p✝ :: Δ✝)
a_ih✝ : ∀ (f : ℕ → SyntacticTerm L), length (rewrite a✝ f) = length a✝
f : ℕ → SyntacticTerm L
⊢ length (Derivation.cast (ex ((Rew.rewrite f) t✝) (Derivation.cast (rewrite a✝ f) ⋯)) ⋯) = length a✝ + 1