Apply df_mend__df_sdrg__df_cytp__df_topsep__df_toplnd__df_rcl__df_he__ax_frege1__ax_frege2__ax_frege8__ax_frege28__ax_frege31__ax_frege41__ax_frege52a__ax_frege54a__ax_frege58a__ax_frege52c__ax_frege54c with ∀ x0 x1 : ι → ο . wb (whe x0 x1) (wss (cima x1 x0) x0).

Assume H0: wceq cmend (cmpt (λ x0 . cvv) (λ x0 . csb (co (cv x0) (cv x0) clmhm) (λ x1 . cun (ctp (cop (cfv cnx cbs) (cv x1)) (cop (cfv cnx cplusg) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . co (cv x2) (cv x3) (cof (cfv (cv x0) cplusg))))) (cop (cfv cnx cmulr) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . ccom (cv x2) (cv x3))))) (cpr (cop (cfv cnx csca) (cfv (cv x0) csca)) (cop (cfv cnx cvsca) (cmpt2 (λ x2 x3 . cfv (cfv (cv x0) csca) cbs) (λ x2 x3 . cv x1) (λ x2 x3 . co (cxp (cfv (cv x0) cbs) (csn (cv x2))) (cv x3) (cof (cfv (cv x0) cvsca))))))))).

Assume H1: wceq csdrg (cmpt (λ x0 . cdr) (λ x0 . crab (λ x1 . wcel (co (cv x0) (cv x1) cress) cdr) (λ x1 . cfv (cv x0) csubrg))).

Assume H2: wceq ccytp (cmpt (λ x0 . cn) (λ x0 . co (cfv (cfv ccnfld cpl1) cmgp) (cmpt (λ x1 . cima (ccnv (cfv (co (cfv ccnfld cmgp) (cdif cc (csn cc0)) cress) cod)) (csn (cv x0))) (λ x1 . co (cfv ccnfld cv1) (cfv (cv x1) (cfv (cfv ccnfld cpl1) cascl)) (cfv (cfv ccnfld cpl1) csg))) cgsu)).

Assume H3: wceq ctopsep (crab (λ x0 . wrex (λ x1 . wa (wbr (cv x1) com cdom) (wceq (cfv (cv x1) (cfv (cv x0) ccl)) (cuni (cv x0)))) (λ x1 . cpw (cuni (cv x0)))) (λ x0 . ctop)).

Assume H4: wceq ctoplnd (crab (λ x0 . wral (λ x1 . wceq (cuni (cv x0)) (cuni (cv x1)) ⟶ wrex (λ x2 . wa (wbr (cv x2) com cdom) (wceq (cuni (cv x0)) (cuni (cv x2)))) (λ x2 . cpw (cv x0))) (λ x1 . cpw (cv x0))) ...).

...

■

Proofgold Proof