Proofgold Proof

Apply df_vrgp__df_cmn__df_abl__df_cyg__df_dprd__df_dpj__df_mgp__df_ur__df_srg__df_ring__df_cring__df_oppr__df_dvdsr__df_unit__df_irred__df_invr__df_dvr__df_rprm with wceq csrg (crab (λ x0 . wa (wcel (cfv (cv x0) cmgp) cmnd) (wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wral (λ x5 . wa (wral (λ x6 . wral (λ x7 . wa (wceq (co (cv x5) (co (cv x6) (cv x7) (cv x2)) (cv x3)) (co (co (cv x5) (cv x6) (cv x3)) (co (cv x5) (cv x7) (cv x3)) (cv x2))) (wceq (co (co (cv x5) (cv x6) (cv x2)) (cv x7) (cv x3)) (co (co (cv x5) (cv x7) (cv x3)) (co (cv x6) (cv x7) (cv x3)) (cv x2)))) (λ x7 . cv x1)) (λ x6 . cv x1)) (wa (wceq (co (cv x4) (cv x5) (cv x3)) (cv x4)) (wceq (co (cv x5) (cv x4) (cv x3)) (cv x4)))) (λ x5 . cv x1)) (cfv (cv x0) c0g)) (cfv (cv x0) cmulr)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs))) (λ x0 . ccmn)).