exact ⟨ofSubformula_toSubformula p (by simp at h; exact h.1), ofSubformula_toSubformula q (by simp at h; exact h.2)⟩
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.or q).bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p ∧ ↑(ofSubformula (q.toSubformula ⋯)) = q
no goals