ext x <;> simp[Rew.comp_app, Fin.eq_zero]
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticSemiformula L 1
⊢ Rew.comp Rew.free (Rew.rewrite fun x => Rew.bShift (f x)) = (Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).comp Rew.free
no goals