Apply df_sslt__df_scut__df_made__df_old__df_new__df_left__df_right__df_txp__df_pprod__df_sset__df_trans__df_bigcup__df_fix__df_limits__df_funs__df_singleton__df_singles__df_image with
wceq csslt (copab (λ x0 x1 . w3a (wss (cv x0) csur) (wss (cv x1) csur) (wral (λ x2 . wral (λ x3 . wbr (cv x2) (cv x3) cslt) (λ x3 . cv x1)) (λ x2 . cv x0)))).