simp[←Rew.hom_comp_app]
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
t : Semiterm L ℕ 0
p : SyntacticSemiformula L 1
⊢ (Rew.rewrite f).hom ([→ t].hom p) = [→ (Rew.rewrite f) t].hom ((Rew.rewrite (⇑Rew.bShift ∘ f)).hom p)
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
t : Semiterm L ℕ 0
p : SyntacticSemiformula L 1
⊢ ((Rew.rewrite f).comp [→ t]).hom p = ([→ (Rew.rewrite f) t].comp (Rew.rewrite (⇑Rew.bShift ∘ f))).hom p