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