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