Apply df_gbow__df_gbo__ax_bgbltosilva__ax_tgoldbachgt__ax_hgprmladder__ax_bgbltosilvaOLD__ax_hgprmladderOLD__ax_tgoldbachgtOLD__df_upwlks__df_spr__df_mgmhm__df_submgm__df_cllaw__df_comlaw__df_asslaw__df_intop__df_clintop__df_assintop with
wceq casslaw (copab (λ x0 x1 . wral (λ x2 . wral (λ x3 . wral (λ x4 . wceq (co (co (cv x2) (cv x3) (cv x0)) (cv x4) (cv x0)) (co (cv x2) (co (cv x3) (cv x4) (cv x0)) (cv x0))) (λ x4 . cv x1)) (λ x3 . cv x1)) (λ x2 . cv x1))).