simp[←Rew.hom_comp_app]
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticFormula L
⊢ (Rew.hom ⇑) ((Rew.rewrite f).hom p) = (Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).hom ((Rew.hom ⇑) p)
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticFormula L
⊢ (Rew.comp ⇑ (Rew.rewrite f)).hom p = ((Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).comp ⇑).hom p