Apply df_vts__ax_hgt749__ax_ros335__ax_ros336__df_trkg2d__df_afs__df_bnj17__df_bnj14__df_bnj13__df_bnj15__df_bnj18__df_bnj19__ax_7d__ax_8d__ax_9d1__ax_9d2__ax_10d__ax_11d with
∀ x0 x1 . (∀ x2 . wceq (cv x2) (cv x1)) ⟶ ∀ x2 . wceq (cv x2) (cv x0).