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 : ι → ο . wb (w_bnj13 x0 x1) (wral (λ x2 . wcel (c_bnj14 x0 x1 (cv x2)) cvv) (λ x2 . x0)).