Apply df_inv__df_iso__df_cic__df_ssc__df_resc__df_subc__df_func__df_idfu__df_cofu__df_resf__df_full__df_fth__df_nat__df_fuc__df_inito__df_termo__df_zeroo__df_doma with wceq czeroo (cmpt (λ x0 . ccat) (λ x0 . cin (cfv (cv x0) cinito) (cfv (cv x0) ctermo))).

Assume H0: wceq cinv (cmpt (λ x0 . ccat) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cin (co (cv x1) (cv x2) (cfv (cv x0) csect)) (ccnv (co (cv x2) (cv x1) (cfv (cv x0) csect)))))).

Assume H1: wceq ciso (cmpt (λ x0 . ccat) (λ x0 . ccom (cmpt (λ x1 . cvv) (λ x1 . cdm (cv x1))) (cfv (cv x0) cinv))).

Assume H2: wceq ccic (cmpt (λ x0 . ccat) (λ x0 . co (cfv (cv x0) ciso) c0 csupp)).

Assume H3: wceq cssc (copab (λ x0 x1 . wex (λ x2 . wa (wfn (cv x1) (cxp (cv x2) (cv x2))) (wrex (λ x3 . wcel (cv x0) (cixp (λ x4 . cxp (cv x3) (cv x3)) (λ x4 . cpw (cfv (cv x4) (cv x1))))) (λ x3 . cpw (cv x2)))))).

Assume H4: wceq cresc (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (co (cv x0) (cdm (cdm (cv x1))) cress) (cop (cfv cnx chom) (cv x1)) csts)).

Assume H5: wceq csubc (cmpt (λ x0 . ccat) (λ x0 . cab (λ x1 . wa (wbr (cv x1) (cfv (cv x0) chomf) cssc) (wsbc (λ x2 . wral (λ x3 . wa (wcel (cfv (cv x3) (cfv (cv x0) ccid)) (co (cv x3) (cv x3) (cv x1))) (wral (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . wcel (co (cv x7) (cv x6) (co (cop (cv x3) (cv x4)) (cv x5) (cfv (cv x0) cco))) (co (cv x3) (cv x5) (cv x1))) (λ x7 . co (cv x4) (cv x5) (cv x1))) (λ x6 . co (cv x3) (cv x4) (cv x1))) (λ x5 . cv x2)) (λ x4 . cv x2))) (λ x3 . cv x2)) (cdm (cdm (cv x1))))))).

Assume H6: wceq cfunc ....

...

■

Proofgold Proof