exact Semiformula.rew_eq_of_funEqOn (by simp[Rew.comp_app, Fin.eq_zero])
  (fun x hx => by simp[Rew.comp_app]; rintro rfl; contradiction)
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
no goals