Apply df_met__df_bl__df_mopn__df_fbas__df_fg__df_metu__df_cnfld__df_zring__df_zrh__df_zlm__df_chr__df_zn__df_refld__df_phl__df_ipf__df_ocv__df_css__df_thl with wceq cfg (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cfv (cv x0) cfbas) (λ x0 x1 . crab (λ x2 . wne (cin (cv x1) (cpw (cv x2))) c0) (λ x2 . cpw (cv x0)))).

Assume H0: wceq cme (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wral (λ x3 . wa (wb (wceq (co (cv x2) (cv x3) (cv x1)) cc0) (wceq (cv x2) (cv x3))) (wral (λ x4 . wbr (co (cv x2) (cv x3) (cv x1)) (co (co (cv x4) (cv x2) (cv x1)) (co (cv x4) (cv x3) (cv x1)) caddc) cle) (λ x4 . cv x0))) (λ x3 . cv x0)) (λ x2 . cv x0)) (λ x1 . co cr (cxp (cv x0) (cv x0)) cmap))).

Assume H1: wceq cbl (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cdm (cdm (cv x0))) (λ x1 x2 . cxr) (λ x1 x2 . crab (λ x3 . wbr (co (cv x1) (cv x3) (cv x0)) (cv x2) clt) (λ x3 . cdm (cdm (cv x0)))))).

Assume H2: wceq cmopn (cmpt (λ x0 . cuni (crn cxmt)) (λ x0 . cfv (crn (cfv (cv x0) cbl)) ctg)).

Assume H3: wceq cfbas (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . w3a (wne (cv x1) c0) (wnel c0 (cv x1)) (wral (λ x2 . wral (λ x3 . wne (cin (cv x1) (cpw (cin (cv x2) (cv x3)))) c0) (λ x3 . cv x1)) (λ x2 . cv x1))) (λ x1 . cpw (cpw (cv x0))))).

Assume H4: wceq cfg (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cfv (cv x0) cfbas) (λ x0 x1 . crab (λ x2 . wne (cin (cv x1) (cpw (cv x2))) c0) (λ x2 . cpw (cv x0)))).

Assume H5: wceq cmetu (cmpt (λ x0 . cuni (crn cpsmet)) (λ x0 . co (cxp (cdm (cdm (cv x0))) (cdm (cdm (cv x0)))) (crn (cmpt (λ x1 . crp) (λ x1 . cima (ccnv (cv x0)) (co cc0 (cv x1) cico)))) cfg)).

...

■

Proofgold Proof