Apply df_coda__df_homa__df_arw__df_ida__df_coa__df_setc__df_catc__df_estrc__df_xpc__df_1stf__df_2ndf__df_prf__df_evlf__df_curf__df_uncf__df_diag__df_hof__df_yon with wceq cdiag (cmpt2 (λ x0 x1 . ccat) (λ x0 x1 . ccat) (λ x0 x1 . co (cop (cv x0) (cv x1)) (co (cv x0) (cv x1) c1stf) ccurf)).

Assume H0: wceq ccoda (ccom c2nd c1st).

Assume H1: wceq choma (cmpt (λ x0 . ccat) (λ x0 . cmpt (λ x1 . cxp (cfv (cv x0) cbs) (cfv (cv x0) cbs)) (λ x1 . cxp (csn (cv x1)) (cfv (cv x1) (cfv (cv x0) chom))))).

Assume H2: wceq carw (cmpt (λ x0 . ccat) (λ x0 . cuni (crn (cfv (cv x0) choma)))).

Assume H3: wceq cida (cmpt (λ x0 . ccat) (λ x0 . cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . cotp (cv x1) (cv x1) (cfv (cv x1) (cfv (cv x0) ccid))))).

Assume H4: wceq ccoa (cmpt (λ x0 . ccat) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) carw) (λ x1 x2 . crab (λ x3 . wceq (cfv (cv x3) ccoda) (cfv (cv x1) cdoma)) (λ x3 . cfv (cv x0) carw)) (λ x1 x2 . cotp (cfv (cv x2) cdoma) (cfv (cv x1) ccoda) (co (cfv (cv x1) c2nd) (cfv (cv x2) c2nd) (co (cop (cfv (cv x2) cdoma) (cfv (cv x1) cdoma)) (cfv (cv x1) ccoda) (cfv (cv x0) cco)))))).

Assume H5: wceq csetc (cmpt (λ x0 . cvv) (λ x0 . ctp (cop (cfv cnx cbs) (cv x0)) (cop (cfv cnx chom) (cmpt2 (λ x1 x2 . cv x0) (λ x1 x2 . cv x0) (λ x1 x2 . co (cv x2) (cv x1) cmap))) (cop (cfv cnx cco) (cmpt2 (λ x1 x2 . cxp (cv x0) (cv x0)) (λ x1 x2 . cv x0) (λ x1 x2 . cmpt2 (λ x3 x4 . co (cv x2) (cfv (cv x1) c2nd) cmap) (λ x3 x4 . co (cfv (cv x1) c2nd) (cfv (cv x1) c1st) cmap) (λ x3 x4 . ccom (cv x3) (cv x4))))))).

Assume H6: wceq ccatc (cmpt (λ x0 . cvv) (λ x0 . csb (cin (cv x0) ccat) (λ x1 . ctp (cop (cfv cnx cbs) ...) ... ...))).

...

■

Proofgold Proof