simp[ofSubformula, toSubformula]
L : Language
μ : Type v
x✝ : ℕ
p : Semiformula L μ (x✝ + 1)
⊢ (↑(ofSubformula (∀' p))).toSubformula ⋯ = ∀' p
L : Language
μ : Type v
x✝ : ℕ
p : Semiformula L μ (x✝ + 1)
⊢ (↑(ofSubformula p)).toSubformula ⋯ = p