Proofgold Address

Known df_ordt__df_xrs__df_qtop__df_imas__df_qus__df_xps__df_mre__df_mrc__df_mri__df_acs__df_cat__df_cid__df_homf__df_comf__df_oppc__df_mon__df_epi__df_sect : ∀ x0 : ο . (wceq cordt (cmpt (λ x1 . cvv) (λ x1 . cfv (cfv (cun (csn (cdm (cv x1))) (crn (cun (cmpt (λ x2 . cdm (cv x1)) (λ x2 . crab (λ x3 . wn (wbr (cv x3) (cv x2) (cv x1))) (λ x3 . cdm (cv x1)))) (cmpt (λ x2 . cdm (cv x1)) (λ x2 . crab (λ x3 . wn (wbr (cv x2) (cv x3) (cv x1))) (λ x3 . cdm (cv x1))))))) cfi) ctg)) ⟶ wceq cxrs (cun (ctp (cop (cfv cnx cbs) cxr) (cop (cfv cnx cplusg) cxad) (cop (cfv cnx cmulr) cxmu)) (ctp (cop (cfv cnx cts) (cfv cle cordt)) (cop (cfv cnx cple) cle) (cop (cfv cnx cds) (cmpt2 (λ x1 x2 . cxr) (λ x1 x2 . cxr) (λ x1 x2 . cif (wbr (cv x1) (cv x2) cle) (co (cv x2) (cxne (cv x1)) cxad) (co (cv x1) (cxne (cv x2)) cxad)))))) ⟶ wceq cqtop (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . crab (λ x3 . wcel (cin (cima (ccnv (cv x2)) (cv x3)) (cuni (cv x1))) (cv x1)) (λ x3 . cpw (cima (cv x2) (cuni (cv x1)))))) ⟶ wceq cimas (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (cfv (cv x2) cbs) (λ x3 . cun (cun (ctp (cop (cfv cnx cbs) (crn (cv x1))) (cop (cfv cnx cplusg) (ciun (λ x4 . cv x3) (λ x4 . ciun (λ x5 . cv x3) (λ x5 . csn (cop (cop (cfv (cv x4) (cv x1)) (cfv (cv x5) (cv x1))) (cfv (co (cv x4) (cv x5) (cfv (cv x2) cplusg)) (cv x1))))))) (cop (cfv cnx cmulr) (ciun (λ x4 . cv x3) (λ x4 . ciun (λ x5 . cv x3) (λ x5 . csn (cop (cop (cfv (cv x4) (cv x1)) (cfv (cv x5) (cv x1))) (cfv (co (cv x4) (cv x5) (cfv (cv x2) cmulr)) (cv x1)))))))) (ctp (cop (cfv cnx csca) (cfv (cv x2) csca)) (cop (cfv cnx cvsca) (ciun (λ x4 . cv x3) (λ x4 . cmpt2 (λ x5 x6 . cfv (cfv (cv x2) csca) cbs) (λ x5 x6 . csn (cfv (cv x4) (cv x1))) (λ x5 x6 . cfv (co (cv x5) (cv x4) (cfv (cv x2) cvsca)) (cv x1))))) (cop (cfv cnx cip) (ciun (λ x4 . cv x3) (λ x4 . ciun (λ x5 . cv x3) (λ x5 . csn (cop (cop (cfv (cv x4) (cv x1)) (cfv (cv x5) (cv x1))) (co (cv x4) (cv x5) (cfv (cv x2) cip))))))))) (ctp (cop (cfv cnx cts) (co (cfv (cv x2) ctopn) (cv x1) cqtop)) (cop (cfv cnx cple) (ccom (ccom (cv x1) (cfv (cv x2) cple)) (ccnv (cv x1)))) (cop (cfv cnx cds) (cmpt2 (λ x4 x5 . crn (cv x1)) (λ x4 x5 . crn (cv x1)) (λ x4 x5 . cinf (ciun (λ x6 . cn) (λ x6 . crn (cmpt (λ x7 . crab (λ x8 . w3a (wceq (cfv (cfv (cfv c1 (cv x8)) c1st) (cv x1)) (cv x4)) (wceq (cfv (cfv (cfv (cv x6) (cv x8)) c2nd) (cv x1)) (cv x5)) (wral (λ x9 . wceq (cfv (cfv (cfv (cv x9) (cv x8)) c2nd) (cv x1)) (cfv (cfv (cfv (co (cv x9) c1 caddc) (cv x8)) c1st) (cv x1))) (λ x9 . co c1 (co (cv x6) c1 cmin) cfz))) (λ x8 . co (cxp (cv x3) (cv x3)) (co c1 (cv x6) cfz) cmap)) (λ x7 . co cxrs (ccom (cfv (cv x2) cds) (cv x7)) cgsu)))) cxr clt))))))) ⟶ wceq cqus (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (cmpt (λ x3 . cfv (cv x1) cbs) (λ x3 . cec (cv x3) (cv x2))) (cv x1) cimas)) ⟶ wceq cxps (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (ccnv (cmpt2 (λ x3 x4 . cfv (cv x1) cbs) (λ x3 x4 . cfv (cv x2) cbs) (λ x3 x4 . ccnv (co (csn (cv x3)) (csn (cv x4)) ccda)))) (co (cfv (cv x1) csca) (ccnv (co (csn (cv x1)) (csn (cv x2)) ccda)) cprds) cimas)) ⟶ wceq cmre (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wa (wcel (cv x1) (cv x2)) (wral (λ x3 . wne (cv x3) c0 ⟶ wcel (cint (cv x3)) (cv x2)) (λ x3 . cpw (cv x2)))) (λ x2 . cpw (cpw (cv x1))))) ⟶ wceq cmrc (cmpt (λ x1 . cuni (crn cmre)) (λ x1 . cmpt (λ x2 . cpw (cuni (cv x1))) (λ x2 . cint (crab (λ x3 . wss (cv x2) (cv x3)) (λ x3 . cv x1))))) ⟶ wceq cmri (cmpt (λ x1 . cuni (crn cmre)) (λ x1 . crab (λ x2 . wral (λ x3 . wn (wcel (cv x3) (cfv (cdif (cv x2) (csn (cv x3))) (cfv (cv x1) cmrc)))) (λ x3 . cv x2)) (λ x2 . cpw (cuni (cv x1))))) ⟶ wceq cacs (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wex (λ x3 . wa (wf (cpw (cv x1)) (cpw (cv x1)) (cv x3)) (wral (λ x4 . wb (wcel (cv x4) (cv x2)) (wss (cuni (cima (cv x3) (cin (cpw (cv x4)) cfn))) (cv x4))) (λ x4 . cpw (cv x1))))) (λ x2 . cfv (cv x1) cmre))) ⟶ wceq ccat (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wral (λ x5 . wa (wrex (λ x6 . wral (λ x7 . wa (wral (λ x8 . wceq (co (cv x6) (cv x8) (co (cop (cv x7) (cv x5)) (cv x5) (cv x4))) (cv x8)) (λ x8 . co (cv x7) (cv x5) (cv x3))) (wral (λ x8 . wceq (co (cv x8) (cv x6) (co (cop (cv x5) (cv x5)) (cv x7) (cv x4))) (cv x8)) (λ x8 . co (cv x5) (cv x7) (cv x3)))) (λ x7 . cv x2)) (λ x6 . co (cv x5) (cv x5) (cv x3))) (wral (λ x6 . wral (λ x7 . wral (λ x8 . wral (λ x9 . wa (wcel (co (cv x9) (cv x8) (co (cop (cv x5) (cv x6)) (cv x7) (cv x4))) (co (cv x5) (cv x7) (cv x3))) (wral (λ x10 . wral (λ x11 . wceq (co (co (cv x11) (cv x9) (co (cop (cv x6) (cv x7)) (cv x10) (cv x4))) (cv x8) (co (cop (cv x5) (cv x6)) (cv x10) (cv x4))) (co (cv x11) (co (cv x9) (cv x8) (co (cop (cv x5) (cv x6)) (cv x7) (cv x4))) (co (cop (cv x5) (cv x7)) (cv x10) (cv x4)))) (λ x11 . co (cv x7) (cv x10) (cv x3))) (λ x10 . cv x2))) (λ x9 . co (cv x6) (cv x7) (cv x3))) (λ x8 . co (cv x5) (cv x6) (cv x3))) (λ x7 . cv x2)) (λ x6 . cv x2))) (λ x5 . cv x2)) (cfv (cv x1) cco)) (cfv (cv x1) chom)) (cfv (cv x1) cbs))) ⟶ wceq ccid (cmpt (λ x1 . ccat) (λ x1 . csb (cfv (cv x1) cbs) (λ x2 . csb (cfv (cv x1) chom) (λ x3 . csb (cfv (cv x1) cco) (λ x4 . cmpt (λ x5 . cv x2) (λ x5 . crio (λ x6 . wral (λ x7 . wa (wral (λ x8 . wceq (co (cv x6) (cv x8) (co (cop (cv x7) (cv x5)) (cv x5) (cv x4))) (cv x8)) (λ x8 . co (cv x7) (cv x5) (cv x3))) (wral (λ x8 . wceq (co (cv x8) (cv x6) (co (cop (cv x5) (cv x5)) (cv x7) (cv x4))) (cv x8)) (λ x8 . co (cv x5) (cv x7) (cv x3)))) (λ x7 . cv x2)) (λ x6 . co (cv x5) (cv x5) (cv x3)))))))) ⟶ wceq chomf (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . co (cv x2) (cv x3) (cfv (cv x1) chom)))) ⟶ wceq ccomf (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cxp (cfv (cv x1) cbs) (cfv (cv x1) cbs)) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cmpt2 (λ x4 x5 . co (cfv (cv x2) c2nd) (cv x3) (cfv (cv x1) chom)) (λ x4 x5 . cfv (cv x2) (cfv (cv x1) chom)) (λ x4 x5 . co (cv x4) (cv x5) (co (cv x2) (cv x3) (cfv (cv x1) cco)))))) ⟶ wceq coppc (cmpt (λ x1 . cvv) (λ x1 . co (co (cv x1) (cop (cfv cnx chom) (ctpos (cfv (cv x1) chom))) csts) (cop (cfv cnx cco) (cmpt2 (λ x2 x3 . cxp (cfv (cv x1) cbs) (cfv (cv x1) cbs)) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . ctpos (co (cop (cv x3) (cfv (cv x2) c2nd)) (cfv (cv x2) c1st) (cfv (cv x1) cco))))) csts)) ⟶ wceq cmon (cmpt (λ x1 . ccat) (λ x1 . csb (cfv (cv x1) cbs) (λ x2 . csb (cfv (cv x1) chom) (λ x3 . cmpt2 (λ x4 x5 . cv x2) (λ x4 x5 . cv x2) (λ x4 x5 . crab (λ x6 . wral (λ x7 . wfun (ccnv (cmpt (λ x8 . co (cv x7) (cv x4) (cv x3)) (λ x8 . co (cv x6) (cv x8) (co (cop (cv x7) (cv x4)) (cv x5) (cfv (cv x1) cco)))))) (λ x7 . cv x2)) (λ x6 . co (cv x4) (cv x5) (cv x3))))))) ⟶ wceq cepi (cmpt (λ x1 . ccat) (λ x1 . ctpos (cfv (cfv (cv x1) coppc) cmon))) ⟶ wceq csect (cmpt (λ x1 . ccat) (λ x1 . cmpt2 (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . copab (λ x4 x5 . wsbc (λ x6 . wa (wa (wcel (cv x4) (co (cv x2) (cv x3) (cv x6))) (wcel (cv x5) (co (cv x3) (cv x2) (cv x6)))) (wceq (co (cv x5) (cv x4) (co (cop (cv x2) (cv x3)) (cv x2) (cfv (cv x1) cco))) (cfv (cv x2) (cfv (cv x1) ccid)))) (cfv (cv x1) chom))))) ⟶ x0) ⟶ x0
Theorem df_ordt : wceq cordt (cmpt (λ x0 . cvv) (λ x0 . cfv (cfv (cun (csn (cdm (cv x0))) (crn (cun (cmpt (λ x1 . cdm (cv x0)) (λ x1 . crab (λ x2 . wn (wbr (cv x2) (cv x1) (cv x0))) (λ x2 . cdm (cv x0)))) (cmpt (λ x1 . cdm (cv x0)) (λ x1 . crab (λ x2 . wn (wbr (cv x1) (cv x2) (cv x0))) (λ x2 . cdm (cv x0))))))) cfi) ctg)) (proof)
Theorem df_xrs : wceq cxrs (cun (ctp (cop (cfv cnx cbs) cxr) (cop (cfv cnx cplusg) cxad) (cop (cfv cnx cmulr) cxmu)) (ctp (cop (cfv cnx cts) (cfv cle cordt)) (cop (cfv cnx cple) cle) (cop (cfv cnx cds) (cmpt2 (λ x0 x1 . cxr) (λ x0 x1 . cxr) (λ x0 x1 . cif (wbr (cv x0) (cv x1) cle) (co (cv x1) (cxne (cv x0)) cxad) (co (cv x0) (cxne (cv x1)) cxad)))))) (proof)
Theorem df_qtop : wceq cqtop (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wcel (cin (cima (ccnv (cv x1)) (cv x2)) (cuni (cv x0))) (cv x0)) (λ x2 . cpw (cima (cv x1) (cuni (cv x0)))))) (proof)
Theorem df_imas : wceq cimas (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (cfv (cv x1) cbs) (λ x2 . cun (cun (ctp (cop (cfv cnx cbs) (crn (cv x0))) (cop (cfv cnx cplusg) (ciun (λ x3 . cv x2) (λ x3 . ciun (λ x4 . cv x2) (λ x4 . csn (cop (cop (cfv (cv x3) (cv x0)) (cfv (cv x4) (cv x0))) (cfv (co (cv x3) (cv x4) (cfv (cv x1) cplusg)) (cv x0))))))) (cop (cfv cnx cmulr) (ciun (λ x3 . cv x2) (λ x3 . ciun (λ x4 . cv x2) (λ x4 . csn (cop (cop (cfv (cv x3) (cv x0)) (cfv (cv x4) (cv x0))) (cfv (co (cv x3) (cv x4) (cfv (cv x1) cmulr)) (cv x0)))))))) (ctp (cop (cfv cnx csca) (cfv (cv x1) csca)) (cop (cfv cnx cvsca) (ciun (λ x3 . cv x2) (λ x3 . cmpt2 (λ x4 x5 . cfv (cfv (cv x1) csca) cbs) (λ x4 x5 . csn (cfv (cv x3) (cv x0))) (λ x4 x5 . cfv (co (cv x4) (cv x3) (cfv (cv x1) cvsca)) (cv x0))))) (cop (cfv cnx cip) (ciun (λ x3 . cv x2) (λ x3 . ciun (λ x4 . cv x2) (λ x4 . csn (cop (cop (cfv (cv x3) (cv x0)) (cfv (cv x4) (cv x0))) (co (cv x3) (cv x4) (cfv (cv x1) cip))))))))) (ctp (cop (cfv cnx cts) (co (cfv (cv x1) ctopn) (cv x0) cqtop)) (cop (cfv cnx cple) (ccom (ccom (cv x0) (cfv (cv x1) cple)) (ccnv (cv x0)))) (cop (cfv cnx cds) (cmpt2 (λ x3 x4 . crn (cv x0)) (λ x3 x4 . crn (cv x0)) (λ x3 x4 . cinf (ciun (λ x5 . cn) (λ x5 . crn (cmpt (λ x6 . crab (λ x7 . w3a (wceq (cfv (cfv (cfv c1 (cv x7)) c1st) (cv x0)) (cv x3)) (wceq (cfv (cfv (cfv (cv x5) (cv x7)) c2nd) (cv x0)) (cv x4)) (wral (λ x8 . wceq (cfv (cfv (cfv (cv x8) (cv x7)) c2nd) (cv x0)) (cfv (cfv (cfv (co (cv x8) c1 caddc) (cv x7)) c1st) (cv x0))) (λ x8 . co c1 (co (cv x5) c1 cmin) cfz))) (λ x7 . co (cxp (cv x2) (cv x2)) (co c1 (cv x5) cfz) cmap)) (λ x6 . co cxrs (ccom (cfv (cv x1) cds) (cv x6)) cgsu)))) cxr clt))))))) (proof)
Theorem df_qus : wceq cqus (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (cmpt (λ x2 . cfv (cv x0) cbs) (λ x2 . cec (cv x2) (cv x1))) (cv x0) cimas)) (proof)
Theorem df_xps : wceq cxps (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (ccnv (cmpt2 (λ x2 x3 . cfv (cv x0) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . ccnv (co (csn (cv x2)) (csn (cv x3)) ccda)))) (co (cfv (cv x0) csca) (ccnv (co (csn (cv x0)) (csn (cv x1)) ccda)) cprds) cimas)) (proof)
Theorem df_mre : wceq cmre (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wa (wcel (cv x0) (cv x1)) (wral (λ x2 . wne (cv x2) c0 ⟶ wcel (cint (cv x2)) (cv x1)) (λ x2 . cpw (cv x1)))) (λ x1 . cpw (cpw (cv x0))))) (proof)
Theorem df_mrc : wceq cmrc (cmpt (λ x0 . cuni (crn cmre)) (λ x0 . cmpt (λ x1 . cpw (cuni (cv x0))) (λ x1 . cint (crab (λ x2 . wss (cv x1) (cv x2)) (λ x2 . cv x0))))) (proof)
Theorem df_mri : wceq cmri (cmpt (λ x0 . cuni (crn cmre)) (λ x0 . crab (λ x1 . wral (λ x2 . wn (wcel (cv x2) (cfv (cdif (cv x1) (csn (cv x2))) (cfv (cv x0) cmrc)))) (λ x2 . cv x1)) (λ x1 . cpw (cuni (cv x0))))) (proof)
Theorem df_acs : wceq cacs (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wex (λ x2 . wa (wf (cpw (cv x0)) (cpw (cv x0)) (cv x2)) (wral (λ x3 . wb (wcel (cv x3) (cv x1)) (wss (cuni (cima (cv x2) (cin (cpw (cv x3)) cfn))) (cv x3))) (λ x3 . cpw (cv x0))))) (λ x1 . cfv (cv x0) cmre))) (proof)
Theorem df_cat : wceq ccat (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wa (wrex (λ x5 . wral (λ x6 . wa (wral (λ x7 . wceq (co (cv x5) (cv x7) (co (cop (cv x6) (cv x4)) (cv x4) (cv x3))) (cv x7)) (λ x7 . co (cv x6) (cv x4) (cv x2))) (wral (λ x7 . wceq (co (cv x7) (cv x5) (co (cop (cv x4) (cv x4)) (cv x6) (cv x3))) (cv x7)) (λ x7 . co (cv x4) (cv x6) (cv x2)))) (λ x6 . cv x1)) (λ x5 . co (cv x4) (cv x4) (cv x2))) (wral (λ x5 . wral (λ x6 . wral (λ x7 . wral (λ x8 . wa (wcel (co (cv x8) (cv x7) (co (cop (cv x4) (cv x5)) (cv x6) (cv x3))) (co (cv x4) (cv x6) (cv x2))) (wral (λ x9 . wral (λ x10 . wceq (co (co (cv x10) (cv x8) (co (cop (cv x5) (cv x6)) (cv x9) (cv x3))) (cv x7) (co (cop (cv x4) (cv x5)) (cv x9) (cv x3))) (co (cv x10) (co (cv x8) (cv x7) (co (cop (cv x4) (cv x5)) (cv x6) (cv x3))) (co (cop (cv x4) (cv x6)) (cv x9) (cv x3)))) (λ x10 . co (cv x6) (cv x9) (cv x2))) (λ x9 . cv x1))) (λ x8 . co (cv x5) (cv x6) (cv x2))) (λ x7 . co (cv x4) (cv x5) (cv x2))) (λ x6 . cv x1)) (λ x5 . cv x1))) (λ x4 . cv x1)) (cfv (cv x0) cco)) (cfv (cv x0) chom)) (cfv (cv x0) cbs))) (proof)
Theorem df_cid : wceq ccid (cmpt (λ x0 . ccat) (λ x0 . csb (cfv (cv x0) cbs) (λ x1 . csb (cfv (cv x0) chom) (λ x2 . csb (cfv (cv x0) cco) (λ x3 . cmpt (λ x4 . cv x1) (λ x4 . crio (λ x5 . wral (λ x6 . wa (wral (λ x7 . wceq (co (cv x5) (cv x7) (co (cop (cv x6) (cv x4)) (cv x4) (cv x3))) (cv x7)) (λ x7 . co (cv x6) (cv x4) (cv x2))) (wral (λ x7 . wceq (co (cv x7) (cv x5) (co (cop (cv x4) (cv x4)) (cv x6) (cv x3))) (cv x7)) (λ x7 . co (cv x4) (cv x6) (cv x2)))) (λ x6 . cv x1)) (λ x5 . co (cv x4) (cv x4) (cv x2)))))))) (proof)
Theorem df_homf : wceq chomf (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . co (cv x1) (cv x2) (cfv (cv x0) chom)))) (proof)
Theorem df_comf : wceq ccomf (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cxp (cfv (cv x0) cbs) (cfv (cv x0) cbs)) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cmpt2 (λ x3 x4 . co (cfv (cv x1) c2nd) (cv x2) (cfv (cv x0) chom)) (λ x3 x4 . cfv (cv x1) (cfv (cv x0) chom)) (λ x3 x4 . co (cv x3) (cv x4) (co (cv x1) (cv x2) (cfv (cv x0) cco)))))) (proof)
Theorem df_oppc : wceq coppc (cmpt (λ x0 . cvv) (λ x0 . co (co (cv x0) (cop (cfv cnx chom) (ctpos (cfv (cv x0) chom))) csts) (cop (cfv cnx cco) (cmpt2 (λ x1 x2 . cxp (cfv (cv x0) cbs) (cfv (cv x0) cbs)) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . ctpos (co (cop (cv x2) (cfv (cv x1) c2nd)) (cfv (cv x1) c1st) (cfv (cv x0) cco))))) csts)) (proof)
Theorem df_mon : wceq cmon (cmpt (λ x0 . ccat) (λ x0 . csb (cfv (cv x0) cbs) (λ x1 . csb (cfv (cv x0) chom) (λ x2 . cmpt2 (λ x3 x4 . cv x1) (λ x3 x4 . cv x1) (λ x3 x4 . crab (λ x5 . wral (λ x6 . wfun (ccnv (cmpt (λ x7 . co (cv x6) (cv x3) (cv x2)) (λ x7 . co (cv x5) (cv x7) (co (cop (cv x6) (cv x3)) (cv x4) (cfv (cv x0) cco)))))) (λ x6 . cv x1)) (λ x5 . co (cv x3) (cv x4) (cv x2))))))) (proof)
Theorem df_epi : wceq cepi (cmpt (λ x0 . ccat) (λ x0 . ctpos (cfv (cfv (cv x0) coppc) cmon))) (proof)
Theorem df_sect : wceq csect (cmpt (λ x0 . ccat) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . copab (λ x3 x4 . wsbc (λ x5 . wa (wa (wcel (cv x3) (co (cv x1) (cv x2) (cv x5))) (wcel (cv x4) (co (cv x2) (cv x1) (cv x5)))) (wceq (co (cv x4) (cv x3) (co (cop (cv x1) (cv x2)) (cv x1) (cfv (cv x0) cco))) (cfv (cv x1) (cfv (cv x0) ccid)))) (cfv (cv x0) chom))))) (proof)