Apply df_mgm2__df_cmgm2__df_sgrp2__df_csgrp2__df_rng0__df_rnghomo__df_rngisom__df_rngc__df_rngcALTV__df_ringc__df_ringcALTV__df_dmatalt__df_scmatalt__df_linc__df_lco__df_lininds__df_lindeps__df_fdiv with wceq ccmgm2 (crab (λ x0 . wbr (cfv (cv x0) cplusg) (cfv (cv x0) cbs) ccomlaw) (λ x0 . cmgm2)).

Assume H0: wceq cmgm2 (cab (λ x0 . wbr (cfv (cv x0) cplusg) (cfv (cv x0) cbs) ccllaw)).

Assume H1: wceq ccmgm2 (crab (λ x0 . wbr (cfv (cv x0) cplusg) (cfv (cv x0) cbs) ccomlaw) (λ x0 . cmgm2)).

Assume H2: wceq csgrp2 (crab (λ x0 . wbr (cfv (cv x0) cplusg) (cfv (cv x0) cbs) casslaw) (λ x0 . cmgm2)).

Assume H3: wceq ccsgrp2 (crab (λ x0 . wbr (cfv (cv x0) cplusg) (cfv (cv x0) cbs) ccomlaw) (λ x0 . csgrp2)).

Assume H4: wceq crng (crab (λ x0 . wa (wcel (cfv (cv x0) cmgp) csgrp) (wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wa (wceq (co (cv x4) (co (cv x5) (cv x6) (cv x2)) (cv x3)) (co (co (cv x4) (cv x5) (cv x3)) (co (cv x4) (cv x6) (cv x3)) (cv x2))) (wceq (co (co (cv x4) (cv x5) (cv x2)) (cv x6) (cv x3)) (co (co (cv x4) (cv x6) (cv x3)) (co (cv x5) (cv x6) (cv x3)) (cv x2)))) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1)) (cfv (cv x0) cmulr)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs))) (λ x0 . cabl)).

Assume H5: wceq crngh (cmpt2 (λ x0 x1 . crng) (λ x0 x1 . crng) (λ x0 x1 . csb (cfv (cv x0) cbs) (λ x2 . csb (cfv (cv x1) cbs) (λ x3 . crab (λ x4 . wral (λ x5 . wral (λ x6 . wa (wceq (cfv (co (cv x5) (cv x6) (cfv (cv x0) cplusg)) (cv x4)) (co (cfv (cv x5) (cv x4)) (cfv (cv x6) (cv x4)) (cfv (cv x1) cplusg))) (wceq (cfv (co (cv x5) (cv x6) (cfv (cv x0) ...)) ...) ...)) ...) ...) ...)))).

...

■

Proofgold Proof