simp[←Rew.hom_comp_app]
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
p : SyntacticSemiformula L 1
h : ¬fvar? p m
⊢ (Rew.rewriteMap fun x => if x = m then 0 else x + 1).hom ([→ &m].hom p) = (Rew.hom Rew.free) p
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
p : SyntacticSemiformula L 1
h : ¬fvar? p m
⊢ ((Rew.rewriteMap fun x => if x = m then 0 else x + 1).comp [→ &m]).hom p = (Rew.hom Rew.free) p