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 ccyg (crab (λ x0 . wrex (λ x1 . wceq (crn (cmpt (λ x2 . cz) (λ x2 . co (cv x2) (cv x1) (cfv (cv x0) cmg)))) (cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) cbs)) (λ x0 . cgrp)).

Assume H0: wceq cvrgp (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cv x0) (λ x1 . cec (cs1 (cop (cv x1) c0)) (cfv (cv x0) cefg)))).

Assume H1: wceq ccmn (crab (λ x0 . wral (λ x1 . wral (λ x2 . wceq (co (cv x1) (cv x2) (cfv (cv x0) cplusg)) (co (cv x2) (cv x1) (cfv (cv x0) cplusg))) (λ x2 . cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) cbs)) (λ x0 . cmnd)).

Assume H2: wceq cabl (cin cgrp ccmn).

Assume H3: wceq ccyg (crab (λ x0 . wrex (λ x1 . wceq (crn (cmpt (λ x2 . cz) (λ x2 . co (cv x2) (cv x1) (cfv (cv x0) cmg)))) (cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) cbs)) (λ x0 . cgrp)).

Assume H4: wceq cdprd (cmpt2 (λ x0 x1 . cgrp) (λ x0 x1 . cab (λ x2 . wa (wf (cdm (cv x2)) (cfv (cv x0) csubg) (cv x2)) (wral (λ x3 . wa (wral (λ x4 . wss (cfv (cv x3) (cv x2)) (cfv (cfv (cv x4) (cv x2)) (cfv (cv x0) ccntz))) (λ x4 . cdif (cdm (cv x2)) (csn (cv x3)))) (wceq (cin (cfv (cv x3) (cv x2)) (cfv (cuni (cima (cv x2) (cdif (cdm (cv x2)) (csn (cv x3))))) (cfv (cfv (cv x0) csubg) cmrc))) (csn (cfv (cv x0) c0g)))) (λ x3 . cdm (cv x2))))) (λ x0 x1 . crn (cmpt (λ x2 . crab (λ x3 . wbr (cv x3) (cfv (cv x0) c0g) cfsupp) (λ x3 . cixp (λ x4 . cdm (cv x1)) (λ x4 . cfv (cv x4) (cv x1)))) (λ x2 . co (cv x0) (cv x2) cgsu)))).

Assume H5: wceq cdpj (cmpt2 ... ... ...).

...

■

Proofgold Proof