Theorem: LO.FirstOrder.shifts_cons (Logic/FirstOrder/Basic/Calculus.lean)

State before:
L : Language
n : ℕ
p : SyntacticSemiformula L n
Δ : List (SyntacticSemiformula L n)
⊢ (p :: Δ)⁺ = (Rew.hom ⇑) p :: Δ⁺
Tactic:
simp[shifts]
State after:
no goals