simp[Rew.comp_app, Fin.eq_zero]
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
p : SyntacticSemiformula L 1
h : ¬fvar? p m
⊢ ∀ (x : Fin 1), ((Rew.rewriteMap fun x => if x = m then 0 else x + 1).comp [→ &m]) #x = Rew.free #x
no goals