Apply df_gim__df_gic__df_ga__df_cntz__df_cntr__df_oppg__df_symg__df_pmtr__df_psgn__df_evpm__df_od__df_gex__df_pgp__df_slw__df_lsm__df_pj1__df_efg__df_frgp with wceq cfrgp (cmpt (λ x0 . cvv) (λ x0 . co (cfv (cxp (cv x0) c2o) cfrmd) (cfv (cv x0) cefg) cqus)).

Assume H0: wceq cgim (cmpt2 (λ x0 x1 . cgrp) (λ x0 x1 . cgrp) (λ x0 x1 . crab (λ x2 . wf1o (cfv (cv x0) cbs) (cfv (cv x1) cbs) (cv x2)) (λ x2 . co (cv x0) (cv x1) cghm))).

Assume H1: wceq cgic (cima (ccnv cgim) (cdif cvv c1o)).

Assume H2: wceq cga (cmpt2 (λ x0 x1 . cgrp) (λ x0 x1 . cvv) (λ x0 x1 . csb (cfv (cv x0) cbs) (λ x2 . crab (λ x3 . wral (λ x4 . wa (wceq (co (cfv (cv x0) c0g) (cv x4) (cv x3)) (cv x4)) (wral (λ x5 . wral (λ x6 . wceq (co (co (cv x5) (cv x6) (cfv (cv x0) cplusg)) (cv x4) (cv x3)) (co (cv x5) (co (cv x6) (cv x4) (cv x3)) (cv x3))) (λ x6 . cv x2)) (λ x5 . cv x2))) (λ x4 . cv x1)) (λ x3 . co (cv x1) (cxp (cv x2) (cv x1)) cmap)))).

Assume H3: wceq ccntz (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw (cfv (cv x0) cbs)) (λ x1 . crab (λ x2 . wral (λ x3 . wceq (co (cv x2) (cv x3) (cfv (cv x0) cplusg)) (co (cv x3) (cv x2) (cfv (cv x0) cplusg))) (λ x3 . cv x1)) (λ x2 . cfv (cv x0) cbs)))).

Assume H4: wceq ccntr (cmpt (λ x0 . cvv) (λ x0 . cfv (cfv (cv x0) cbs) (cfv (cv x0) ccntz))).

Assume H5: wceq coppg (cmpt (λ x0 . cvv) (λ x0 . co (cv x0) (cop (cfv cnx cplusg) (ctpos (cfv (cv x0) cplusg))) csts)).

Assume H6: wceq csymg (cmpt (λ x0 . cvv) (λ x0 . csb (cab (λ x1 . wf1o (cv x0) (cv x0) (cv x1))) (λ x1 . ctp (cop (cfv cnx cbs) (cv x1)) (cop (cfv cnx cplusg) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv ...) ...)) ...))).

...

■

Proofgold Proof