Apply df_mend__df_sdrg__df_cytp__df_topsep__df_toplnd__df_rcl__df_he__ax_frege1__ax_frege2__ax_frege8__ax_frege28__ax_frege31__ax_frege41__ax_frege52a__ax_frege54a__ax_frege58a__ax_frege52c__ax_frege54c with
wceq ctopsep (crab (λ x0 . wrex (λ x1 . wa (wbr (cv x1) com cdom) (wceq (cfv (cv x1) (cfv (cv x0) ccl)) (cuni (cv x0)))) (λ x1 . cpw (cuni (cv x0)))) (λ x0 . ctop)).