simp[ofSubformula, toSubformula]
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.ex.bv ≤ x✝
⊢ ↑(ofSubformula (p.ex.toSubformula h)) = p.ex
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.ex.bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p