Theorem: LO.FirstOrder.Derivation.Restricted.length_rewrite (Logic/FirstOrder/Hauptsatz.lean)

State before:
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
C : Set (SyntacticFormula L)
hC : ∀ (f : ℕ → Semiterm L ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ Δ₁ Δ₂ Γ : Sequent L
f : ℕ → SyntacticTerm L
d : ⊢ᶜ[C] Δ
⊢ length ↑(rewrite hC f d) = length ↑d
Tactic:
simp[rewrite]
State after:
no goals