Apply df_trls__df_trlson__df_pths__df_spths__df_pthson__df_spthson__df_clwlks__df_crcts__df_cycls__df_wwlks__df_wwlksn__df_wwlksnon__df_wspthsn__df_wspthsnon__df_clwwlk__df_clwwlkn__df_clwwlknOLD__df_clwwlknon with
wceq cspthson (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cvtx) (λ x1 x2 . cfv (cv x0) cvtx) (λ x1 x2 . copab (λ x3 x4 . wa (wbr (cv x3) (cv x4) (co (cv x1) (cv x2) (cfv (cv x0) ctrlson))) (wbr (cv x3) (cv x4) (cfv (cv x0) cspths)))))).