intro p hp
case a
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p q r : SyntacticFormula L
m : ℕ
Δ : Sequent L
h : ∀ p ∈ Δ, ¬fvar? p m
⊢ ∀ x ∈ Δ, (Rew.rewriteMap fun x => if x = m then 0 else x + 1).hom x = (Rew.hom ⇑) x
case a
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
Δ : Sequent L
h : ∀ p ∈ Δ, ¬fvar? p m
p : Semiformula L ℕ 0
hp : p ∈ Δ
⊢ (Rew.rewriteMap fun x => if x = m then 0 else x + 1).hom p = (Rew.hom ⇑) p