Apply df_dip__df_ssp__df_lno__df_nmoo__df_blo__df_0o__df_aj__df_hmo__df_ph__df_cbn__df_hlo__df_hnorm__df_hba__df_h0v__df_hvsub__df_hlim__df_hcau__ax_hilex with wceq ccbn (crab (λ x0 . wcel (cfv (cv x0) cims) (cfv (cfv (cv x0) cba) cms)) (λ x0 . cnv)).

Assume H0: wceq cdip (cmpt (λ x0 . cnv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cba) (λ x1 x2 . cfv (cv x0) cba) (λ x1 x2 . co (csu (co c1 c4 cfz) (λ x3 . co (co ci (cv x3) cexp) (co (cfv (co (cv x1) (co (co ci (cv x3) cexp) (cv x2) (cfv (cv x0) cns)) (cfv (cv x0) cpv)) (cfv (cv x0) cnmcv)) c2 cexp) cmul)) c4 cdiv))).

Assume H1: wceq css (cmpt (λ x0 . cnv) (λ x0 . crab (λ x1 . w3a (wss (cfv (cv x1) cpv) (cfv (cv x0) cpv)) (wss (cfv (cv x1) cns) (cfv (cv x0) cns)) (wss (cfv (cv x1) cnmcv) (cfv (cv x0) cnmcv))) (λ x1 . cnv))).

Assume H2: wceq clno (cmpt2 (λ x0 x1 . cnv) (λ x0 x1 . cnv) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wral (λ x5 . wceq (cfv (co (co (cv x3) (cv x4) (cfv (cv x0) cns)) (cv x5) (cfv (cv x0) cpv)) (cv x2)) (co (co (cv x3) (cfv (cv x4) (cv x2)) (cfv (cv x1) cns)) (cfv (cv x5) (cv x2)) (cfv (cv x1) cpv))) (λ x5 . cfv (cv x0) cba)) (λ x4 . cfv (cv x0) cba)) (λ x3 . cc)) (λ x2 . co (cfv (cv x1) cba) (cfv (cv x0) cba) cmap))).

Assume H3: wceq cnmoo (cmpt2 (λ x0 x1 . cnv) (λ x0 x1 . cnv) (λ x0 x1 . cmpt (λ x2 . co (cfv (cv x1) cba) (cfv (cv x0) cba) cmap) (λ x2 . csup (cab (λ x3 . wrex (λ x4 . wa (wbr (cfv (cv x4) (cfv (cv x0) cnmcv)) c1 cle) (wceq (cv x3) (cfv (cfv (cv x4) (cv x2)) (cfv (cv x1) cnmcv)))) (λ x4 . cfv (cv ...) ...))) ... ...))).

...

■

Proofgold Proof