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