simp[ofSubformula, toSubformula, UTerm.toSubterm_ofSubterm]
L : Language
μ : Type v
x✝ arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝
⊢ (↑(ofSubformula (Semiformula.nrel r v))).toSubformula ⋯ = Semiformula.nrel r v
no goals