Apply df_retr__df_pconn__df_sconn__df_cvm__df_goel__df_gona__df_goal__df_sat__df_sate__df_fmla__df_gonot__df_goan__df_goim__df_goor__df_gobi__df_goeq__df_goex__df_prv with wceq cprv (copab (λ x0 x1 . wceq (co (cv x0) (cv x1) csate) (co (cv x0) com cmap))).

Assume H0: wceq cretr (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . crab (λ x2 . wrex (λ x3 . wne (co (ccom (cv x2) (cv x3)) (cres cid (cuni (cv x0))) (co (cv x0) (cv x0) chtpy)) c0) (λ x3 . co (cv x1) (cv x0) ccn)) (λ x2 . co (cv x0) (cv x1) ccn))).

Assume H1: wceq cpconn (crab (λ x0 . wral (λ x1 . wral (λ x2 . wrex (λ x3 . wa (wceq (cfv cc0 (cv x3)) (cv x1)) (wceq (cfv c1 (cv x3)) (cv x2))) (λ x3 . co cii (cv x0) ccn)) (λ x2 . cuni (cv x0))) (λ x1 . cuni (cv x0))) (λ x0 . ctop)).

Assume H2: wceq csconn (crab (λ x0 . wral (λ x1 . wceq (cfv cc0 (cv x1)) (cfv c1 (cv x1)) ⟶ wbr (cv x1) (cxp (co cc0 c1 cicc) (csn (cfv cc0 (cv x1)))) (cfv (cv x0) cphtpc)) (λ x1 . co cii (cv x0) ccn)) (λ x0 . cpconn)).

Assume H3: wceq ccvm (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wrex (λ x4 . wa (wcel (cv x3) (cv x4)) (wrex (λ x5 . wa (wceq (cuni (cv x5)) (cima (ccnv (cv x2)) (cv x4))) (wral (λ x6 . wa (wral (λ x7 . wceq (cin (cv x6) (cv x7)) c0) (λ x7 . cdif (cv x5) (csn (cv x6)))) (wcel (cres (cv x2) (cv x6)) (co (co (cv x0) (cv x6) crest) (co (cv x1) (cv x4) crest) chmeo))) (λ x6 . cv x5))) (λ x5 . cdif (cpw (cv x0)) (csn c0)))) (λ x4 . cv x1)) (λ x3 . cuni (cv x1))) (λ x2 . co (cv x0) (cv x1) ccn))).

Assume H4: wceq cgoe (cmpt (λ x0 . cxp com com) (λ x0 . cop c0 ...)).

...

■

Proofgold Proof