Proofgold Address

Known 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 : ∀ x0 : ο . (wceq ccoda (ccom c2nd c1st) ⟶ wceq choma (cmpt (λ x1 . ccat) (λ x1 . cmpt (λ x2 . cxp (cfv (cv x1) cbs) (cfv (cv x1) cbs)) (λ x2 . cxp (csn (cv x2)) (cfv (cv x2) (cfv (cv x1) chom))))) ⟶ wceq carw (cmpt (λ x1 . ccat) (λ x1 . cuni (crn (cfv (cv x1) choma)))) ⟶ wceq cida (cmpt (λ x1 . ccat) (λ x1 . cmpt (λ x2 . cfv (cv x1) cbs) (λ x2 . cotp (cv x2) (cv x2) (cfv (cv x2) (cfv (cv x1) ccid))))) ⟶ wceq ccoa (cmpt (λ x1 . ccat) (λ x1 . cmpt2 (λ x2 x3 . cfv (cv x1) carw) (λ x2 x3 . crab (λ x4 . wceq (cfv (cv x4) ccoda) (cfv (cv x2) cdoma)) (λ x4 . cfv (cv x1) carw)) (λ x2 x3 . cotp (cfv (cv x3) cdoma) (cfv (cv x2) ccoda) (co (cfv (cv x2) c2nd) (cfv (cv x3) c2nd) (co (cop (cfv (cv x3) cdoma) (cfv (cv x2) cdoma)) (cfv (cv x2) ccoda) (cfv (cv x1) cco)))))) ⟶ wceq csetc (cmpt (λ x1 . cvv) (λ x1 . ctp (cop (cfv cnx cbs) (cv x1)) (cop (cfv cnx chom) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . co (cv x3) (cv x2) cmap))) (cop (cfv cnx cco) (cmpt2 (λ x2 x3 . cxp (cv x1) (cv x1)) (λ x2 x3 . cv x1) (λ x2 x3 . cmpt2 (λ x4 x5 . co (cv x3) (cfv (cv x2) c2nd) cmap) (λ x4 x5 . co (cfv (cv x2) c2nd) (cfv (cv x2) c1st) cmap) (λ x4 x5 . ccom (cv x4) (cv x5))))))) ⟶ wceq ccatc (cmpt (λ x1 . cvv) (λ x1 . csb (cin (cv x1) ccat) (λ x2 . ctp (cop (cfv cnx cbs) (cv x2)) (cop (cfv cnx chom) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . co (cv x3) (cv x4) cfunc))) (cop (cfv cnx cco) (cmpt2 (λ x3 x4 . cxp (cv x2) (cv x2)) (λ x3 x4 . cv x2) (λ x3 x4 . cmpt2 (λ x5 x6 . co (cfv (cv x3) c2nd) (cv x4) cfunc) (λ x5 x6 . cfv (cv x3) cfunc) (λ x5 x6 . co (cv x5) (cv x6) ccofu))))))) ⟶ wceq cestrc (cmpt (λ x1 . cvv) (λ x1 . ctp (cop (cfv cnx cbs) (cv x1)) (cop (cfv cnx chom) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . co (cfv (cv x3) cbs) (cfv (cv x2) cbs) cmap))) (cop (cfv cnx cco) (cmpt2 (λ x2 x3 . cxp (cv x1) (cv x1)) (λ x2 x3 . cv x1) (λ x2 x3 . cmpt2 (λ x4 x5 . co (cfv (cv x3) cbs) (cfv (cfv (cv x2) c2nd) cbs) cmap) (λ x4 x5 . co (cfv (cfv (cv x2) c2nd) cbs) (cfv (cfv (cv x2) c1st) cbs) cmap) (λ x4 x5 . ccom (cv x4) (cv x5))))))) ⟶ wceq cxpc (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (cxp (cfv (cv x1) cbs) (cfv (cv x2) cbs)) (λ x3 . csb (cmpt2 (λ x4 x5 . cv x3) (λ x4 x5 . cv x3) (λ x4 x5 . cxp (co (cfv (cv x4) c1st) (cfv (cv x5) c1st) (cfv (cv x1) chom)) (co (cfv (cv x4) c2nd) (cfv (cv x5) c2nd) (cfv (cv x2) chom)))) (λ x4 . ctp (cop (cfv cnx cbs) (cv x3)) (cop (cfv cnx chom) (cv x4)) (cop (cfv cnx cco) (cmpt2 (λ x5 x6 . cxp (cv x3) (cv x3)) (λ x5 x6 . cv x3) (λ x5 x6 . cmpt2 (λ x7 x8 . co (cfv (cv x5) c2nd) (cv x6) (cv x4)) (λ x7 x8 . cfv (cv x5) (cv x4)) (λ x7 x8 . cop (co (cfv (cv x7) c1st) (cfv (cv x8) c1st) (co (cop (cfv (cfv (cv x5) c1st) c1st) (cfv (cfv (cv x5) c2nd) c1st)) (cfv (cv x6) c1st) (cfv (cv x1) cco))) (co (cfv (cv x7) c2nd) (cfv (cv x8) c2nd) (co (cop (cfv (cfv (cv x5) c1st) c2nd) (cfv (cfv (cv x5) c2nd) c2nd)) (cfv (cv x6) c2nd) (cfv (cv x2) cco))))))))))) ⟶ wceq c1stf (cmpt2 (λ x1 x2 . ccat) (λ x1 x2 . ccat) (λ x1 x2 . csb (cxp (cfv (cv x1) cbs) (cfv (cv x2) cbs)) (λ x3 . cop (cres c1st (cv x3)) (cmpt2 (λ x4 x5 . cv x3) (λ x4 x5 . cv x3) (λ x4 x5 . cres c1st (co (cv x4) (cv x5) (cfv (co (cv x1) (cv x2) cxpc) chom))))))) ⟶ wceq c2ndf (cmpt2 (λ x1 x2 . ccat) (λ x1 x2 . ccat) (λ x1 x2 . csb (cxp (cfv (cv x1) cbs) (cfv (cv x2) cbs)) (λ x3 . cop (cres c2nd (cv x3)) (cmpt2 (λ x4 x5 . cv x3) (λ x4 x5 . cv x3) (λ x4 x5 . cres c2nd (co (cv x4) (cv x5) (cfv (co (cv x1) (cv x2) cxpc) chom))))))) ⟶ wceq cprf (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (cdm (cfv (cv x1) c1st)) (λ x3 . cop (cmpt (λ x4 . cv x3) (λ x4 . cop (cfv (cv x4) (cfv (cv x1) c1st)) (cfv (cv x4) (cfv (cv x2) c1st)))) (cmpt2 (λ x4 x5 . cv x3) (λ x4 x5 . cv x3) (λ x4 x5 . cmpt (λ x6 . cdm (co (cv x4) (cv x5) (cfv (cv x1) c2nd))) (λ x6 . cop (cfv (cv x6) (co (cv x4) (cv x5) (cfv (cv x1) c2nd))) (cfv (cv x6) (co (cv x4) (cv x5) (cfv (cv x2) c2nd))))))))) ⟶ wceq cevlf (cmpt2 (λ x1 x2 . ccat) (λ x1 x2 . ccat) (λ x1 x2 . cop (cmpt2 (λ x3 x4 . co (cv x1) (cv x2) cfunc) (λ x3 x4 . cfv (cv x1) cbs) (λ x3 x4 . cfv (cv x4) (cfv (cv x3) c1st))) (cmpt2 (λ x3 x4 . cxp (co (cv x1) (cv x2) cfunc) (cfv (cv x1) cbs)) (λ x3 x4 . cxp (co (cv x1) (cv x2) cfunc) (cfv (cv x1) cbs)) (λ x3 x4 . csb (cfv (cv x3) c1st) (λ x5 . csb (cfv (cv x4) c1st) (λ x6 . cmpt2 (λ x7 x8 . co (cv x5) (cv x6) (co (cv x1) (cv x2) cnat)) (λ x7 x8 . co (cfv (cv x3) c2nd) (cfv (cv x4) c2nd) (cfv (cv x1) chom)) (λ x7 x8 . co (cfv (cfv (cv x4) c2nd) (cv x7)) (cfv (cv x8) (co (cfv (cv x3) c2nd) (cfv (cv x4) c2nd) (cfv (cv x5) c2nd))) (co (cop (cfv (cfv (cv x3) c2nd) (cfv (cv x5) c1st)) (cfv (cfv (cv x4) c2nd) (cfv (cv x5) c1st))) (cfv (cfv (cv x4) c2nd) (cfv (cv x6) c1st)) (cfv (cv x2) cco))))))))) ⟶ wceq ccurf (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (cfv (cv x1) c1st) (λ x3 . csb (cfv (cv x1) c2nd) (λ x4 . cop (cmpt (λ x5 . cfv (cv x3) cbs) (λ x5 . cop (cmpt (λ x6 . cfv (cv x4) cbs) (λ x6 . co (cv x5) (cv x6) (cfv (cv x2) c1st))) (cmpt2 (λ x6 x7 . cfv (cv x4) cbs) (λ x6 x7 . cfv (cv x4) cbs) (λ x6 x7 . cmpt (λ x8 . co (cv x6) (cv x7) (cfv (cv x4) chom)) (λ x8 . co (cfv (cv x5) (cfv (cv x3) ccid)) (cv x8) (co (cop (cv x5) (cv x6)) (cop (cv x5) (cv x7)) (cfv (cv x2) c2nd))))))) (cmpt2 (λ x5 x6 . cfv (cv x3) cbs) (λ x5 x6 . cfv (cv x3) cbs) (λ x5 x6 . cmpt (λ x7 . co (cv x5) (cv x6) (cfv (cv x3) chom)) (λ x7 . cmpt (λ x8 . cfv (cv x4) cbs) (λ x8 . co (cv x7) (cfv (cv x8) (cfv (cv x4) ccid)) (co (cop (cv x5) (cv x8)) (cop (cv x6) (cv x8)) (cfv (cv x2) c2nd)))))))))) ⟶ wceq cuncf (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (co (cfv c1 (cv x1)) (cfv c2 (cv x1)) cevlf) (co (co (cv x2) (co (cfv cc0 (cv x1)) (cfv c1 (cv x1)) c1stf) ccofu) (co (cfv cc0 (cv x1)) (cfv c1 (cv x1)) c2ndf) cprf) ccofu)) ⟶ wceq cdiag (cmpt2 (λ x1 x2 . ccat) (λ x1 x2 . ccat) (λ x1 x2 . co (cop (cv x1) (cv x2)) (co (cv x1) (cv x2) c1stf) ccurf)) ⟶ wceq chof (cmpt (λ x1 . ccat) (λ x1 . cop (cfv (cv x1) chomf) (csb (cfv (cv x1) cbs) (λ x2 . cmpt2 (λ x3 x4 . cxp (cv x2) (cv x2)) (λ x3 x4 . cxp (cv x2) (cv x2)) (λ x3 x4 . cmpt2 (λ x5 x6 . co (cfv (cv x4) c1st) (cfv (cv x3) c1st) (cfv (cv x1) chom)) (λ x5 x6 . co (cfv (cv x3) c2nd) (cfv (cv x4) c2nd) (cfv (cv x1) chom)) (λ x5 x6 . cmpt (λ x7 . cfv (cv x3) (cfv (cv x1) chom)) (λ x7 . co (co (cv x6) (cv x7) (co (cv x3) (cfv (cv x4) c2nd) (cfv (cv x1) cco))) (cv x5) (co (cop (cfv (cv x4) c1st) (cfv (cv x3) c1st)) (cfv (cv x4) c2nd) (cfv (cv x1) cco))))))))) ⟶ wceq cyon (cmpt (λ x1 . ccat) (λ x1 . co (cop (cv x1) (cfv (cv x1) coppc)) (cfv (cfv (cv x1) coppc) chof) ccurf)) ⟶ x0) ⟶ x0
Theorem df_coda : wceq ccoda (ccom c2nd c1st) (proof)
Theorem df_homa : 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))))) (proof)
Theorem df_arw : wceq carw (cmpt (λ x0 . ccat) (λ x0 . cuni (crn (cfv (cv x0) choma)))) (proof)
Theorem df_ida : 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))))) (proof)
Theorem df_coa : 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)))))) (proof)
Theorem df_setc : 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))))))) (proof)
Theorem df_catc : wceq ccatc (cmpt (λ x0 . cvv) (λ x0 . csb (cin (cv x0) ccat) (λ x1 . ctp (cop (cfv cnx cbs) (cv x1)) (cop (cfv cnx chom) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . co (cv x2) (cv x3) cfunc))) (cop (cfv cnx cco) (cmpt2 (λ x2 x3 . cxp (cv x1) (cv x1)) (λ x2 x3 . cv x1) (λ x2 x3 . cmpt2 (λ x4 x5 . co (cfv (cv x2) c2nd) (cv x3) cfunc) (λ x4 x5 . cfv (cv x2) cfunc) (λ x4 x5 . co (cv x4) (cv x5) ccofu))))))) (proof)
Theorem df_estrc : wceq cestrc (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 (cfv (cv x2) cbs) (cfv (cv x1) cbs) cmap))) (cop (cfv cnx cco) (cmpt2 (λ x1 x2 . cxp (cv x0) (cv x0)) (λ x1 x2 . cv x0) (λ x1 x2 . cmpt2 (λ x3 x4 . co (cfv (cv x2) cbs) (cfv (cfv (cv x1) c2nd) cbs) cmap) (λ x3 x4 . co (cfv (cfv (cv x1) c2nd) cbs) (cfv (cfv (cv x1) c1st) cbs) cmap) (λ x3 x4 . ccom (cv x3) (cv x4))))))) (proof)
Theorem df_xpc : wceq cxpc (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (cxp (cfv (cv x0) cbs) (cfv (cv x1) cbs)) (λ x2 . csb (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . cxp (co (cfv (cv x3) c1st) (cfv (cv x4) c1st) (cfv (cv x0) chom)) (co (cfv (cv x3) c2nd) (cfv (cv x4) c2nd) (cfv (cv x1) chom)))) (λ x3 . ctp (cop (cfv cnx cbs) (cv x2)) (cop (cfv cnx chom) (cv x3)) (cop (cfv cnx cco) (cmpt2 (λ x4 x5 . cxp (cv x2) (cv x2)) (λ x4 x5 . cv x2) (λ x4 x5 . cmpt2 (λ x6 x7 . co (cfv (cv x4) c2nd) (cv x5) (cv x3)) (λ x6 x7 . cfv (cv x4) (cv x3)) (λ x6 x7 . cop (co (cfv (cv x6) c1st) (cfv (cv x7) c1st) (co (cop (cfv (cfv (cv x4) c1st) c1st) (cfv (cfv (cv x4) c2nd) c1st)) (cfv (cv x5) c1st) (cfv (cv x0) cco))) (co (cfv (cv x6) c2nd) (cfv (cv x7) c2nd) (co (cop (cfv (cfv (cv x4) c1st) c2nd) (cfv (cfv (cv x4) c2nd) c2nd)) (cfv (cv x5) c2nd) (cfv (cv x1) cco))))))))))) (proof)
Theorem df_1stf : wceq c1stf (cmpt2 (λ x0 x1 . ccat) (λ x0 x1 . ccat) (λ x0 x1 . csb (cxp (cfv (cv x0) cbs) (cfv (cv x1) cbs)) (λ x2 . cop (cres c1st (cv x2)) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . cres c1st (co (cv x3) (cv x4) (cfv (co (cv x0) (cv x1) cxpc) chom))))))) (proof)
Theorem df_2ndf : wceq c2ndf (cmpt2 (λ x0 x1 . ccat) (λ x0 x1 . ccat) (λ x0 x1 . csb (cxp (cfv (cv x0) cbs) (cfv (cv x1) cbs)) (λ x2 . cop (cres c2nd (cv x2)) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . cres c2nd (co (cv x3) (cv x4) (cfv (co (cv x0) (cv x1) cxpc) chom))))))) (proof)
Theorem df_prf : wceq cprf (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (cdm (cfv (cv x0) c1st)) (λ x2 . cop (cmpt (λ x3 . cv x2) (λ x3 . cop (cfv (cv x3) (cfv (cv x0) c1st)) (cfv (cv x3) (cfv (cv x1) c1st)))) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . cmpt (λ x5 . cdm (co (cv x3) (cv x4) (cfv (cv x0) c2nd))) (λ x5 . cop (cfv (cv x5) (co (cv x3) (cv x4) (cfv (cv x0) c2nd))) (cfv (cv x5) (co (cv x3) (cv x4) (cfv (cv x1) c2nd))))))))) (proof)
Theorem df_evlf : wceq cevlf (cmpt2 (λ x0 x1 . ccat) (λ x0 x1 . ccat) (λ x0 x1 . cop (cmpt2 (λ x2 x3 . co (cv x0) (cv x1) cfunc) (λ x2 x3 . cfv (cv x0) cbs) (λ x2 x3 . cfv (cv x3) (cfv (cv x2) c1st))) (cmpt2 (λ x2 x3 . cxp (co (cv x0) (cv x1) cfunc) (cfv (cv x0) cbs)) (λ x2 x3 . cxp (co (cv x0) (cv x1) cfunc) (cfv (cv x0) cbs)) (λ x2 x3 . csb (cfv (cv x2) c1st) (λ x4 . csb (cfv (cv x3) c1st) (λ x5 . cmpt2 (λ x6 x7 . co (cv x4) (cv x5) (co (cv x0) (cv x1) cnat)) (λ x6 x7 . co (cfv (cv x2) c2nd) (cfv (cv x3) c2nd) (cfv (cv x0) chom)) (λ x6 x7 . co (cfv (cfv (cv x3) c2nd) (cv x6)) (cfv (cv x7) (co (cfv (cv x2) c2nd) (cfv (cv x3) c2nd) (cfv (cv x4) c2nd))) (co (cop (cfv (cfv (cv x2) c2nd) (cfv (cv x4) c1st)) (cfv (cfv (cv x3) c2nd) (cfv (cv x4) c1st))) (cfv (cfv (cv x3) c2nd) (cfv (cv x5) c1st)) (cfv (cv x1) cco))))))))) (proof)
Theorem df_curf : wceq ccurf (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (cfv (cv x0) c1st) (λ x2 . csb (cfv (cv x0) c2nd) (λ x3 . cop (cmpt (λ x4 . cfv (cv x2) cbs) (λ x4 . cop (cmpt (λ x5 . cfv (cv x3) cbs) (λ x5 . co (cv x4) (cv x5) (cfv (cv x1) c1st))) (cmpt2 (λ x5 x6 . cfv (cv x3) cbs) (λ x5 x6 . cfv (cv x3) cbs) (λ x5 x6 . cmpt (λ x7 . co (cv x5) (cv x6) (cfv (cv x3) chom)) (λ x7 . co (cfv (cv x4) (cfv (cv x2) ccid)) (cv x7) (co (cop (cv x4) (cv x5)) (cop (cv x4) (cv x6)) (cfv (cv x1) c2nd))))))) (cmpt2 (λ x4 x5 . cfv (cv x2) cbs) (λ x4 x5 . cfv (cv x2) cbs) (λ x4 x5 . cmpt (λ x6 . co (cv x4) (cv x5) (cfv (cv x2) chom)) (λ x6 . cmpt (λ x7 . cfv (cv x3) cbs) (λ x7 . co (cv x6) (cfv (cv x7) (cfv (cv x3) ccid)) (co (cop (cv x4) (cv x7)) (cop (cv x5) (cv x7)) (cfv (cv x1) c2nd)))))))))) (proof)
Theorem df_uncf : wceq cuncf (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (co (cfv c1 (cv x0)) (cfv c2 (cv x0)) cevlf) (co (co (cv x1) (co (cfv cc0 (cv x0)) (cfv c1 (cv x0)) c1stf) ccofu) (co (cfv cc0 (cv x0)) (cfv c1 (cv x0)) c2ndf) cprf) ccofu)) (proof)
Theorem df_diag : wceq cdiag (cmpt2 (λ x0 x1 . ccat) (λ x0 x1 . ccat) (λ x0 x1 . co (cop (cv x0) (cv x1)) (co (cv x0) (cv x1) c1stf) ccurf)) (proof)
Theorem df_hof : wceq chof (cmpt (λ x0 . ccat) (λ x0 . cop (cfv (cv x0) chomf) (csb (cfv (cv x0) cbs) (λ x1 . cmpt2 (λ x2 x3 . cxp (cv x1) (cv x1)) (λ x2 x3 . cxp (cv x1) (cv x1)) (λ x2 x3 . cmpt2 (λ x4 x5 . co (cfv (cv x3) c1st) (cfv (cv x2) c1st) (cfv (cv x0) chom)) (λ x4 x5 . co (cfv (cv x2) c2nd) (cfv (cv x3) c2nd) (cfv (cv x0) chom)) (λ x4 x5 . cmpt (λ x6 . cfv (cv x2) (cfv (cv x0) chom)) (λ x6 . co (co (cv x5) (cv x6) (co (cv x2) (cfv (cv x3) c2nd) (cfv (cv x0) cco))) (cv x4) (co (cop (cfv (cv x3) c1st) (cfv (cv x2) c1st)) (cfv (cv x3) c2nd) (cfv (cv x0) cco))))))))) (proof)
Theorem df_yon : wceq cyon (cmpt (λ x0 . ccat) (λ x0 . co (cop (cv x0) (cfv (cv x0) coppc)) (cfv (cfv (cv x0) coppc) chof) ccurf)) (proof)