simp[ofSubformula, toSubformula, UTerm.ofSubterm_toSubterm]
L : Language
μ : Type v
x✝ arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → UTerm L μ
h : (rel r v).bv ≤ x✝
⊢ ↑(ofSubformula ((rel r v).toSubformula h)) = rel r v
no goals