simp[ofSubformula, toSubformula]
L : Language
μ : Type v
x✝ : ℕ
p q : Semiformula L μ x✝
⊢ (↑(ofSubformula (p ⋏ q))).toSubformula ⋯ = p ⋏ q
L : Language
μ : Type v
x✝ : ℕ
p q : Semiformula L μ x✝
⊢ (↑(ofSubformula p)).toSubformula ⋯ = p ∧ (↑(ofSubformula q)).toSubformula ⋯ = q