Apply df_docaN__df_djaN__df_dib__df_dic__df_dih__df_doch__df_djh__df_lpolN__df_lcdual__df_mapd__df_hvmap__df_hdmap1__df_hdmap__df_hgmap__df_hlhil__df_nacs__df_mzpcl__df_mzp with wceq cnacs (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wceq (cv x2) (cfv (cv x3) (cfv (cv x1) cmrc))) (λ x3 . cin (cpw (cv x0)) cfn)) (λ x2 . cv x1)) (λ x1 . cfv (cv x0) cacs))).

Assume H0: wceq cocaN (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt (λ x2 . cpw (cfv (cv x1) (cfv (cv x0) cltrn))) (λ x2 . cfv (co (co (cfv (cfv (cint (crab (λ x3 . wss (cv x2) (cv x3)) (λ x3 . crn (cfv (cv x1) (cfv (cv x0) cdia))))) (ccnv (cfv (cv x1) (cfv (cv x0) cdia)))) (cfv (cv x0) coc)) (cfv (cv x1) (cfv (cv x0) coc)) (cfv (cv x0) cjn)) (cv x1) (cfv (cv x0) cmee)) (cfv (cv x1) (cfv (cv x0) cdia)))))).

Assume H1: wceq cdjaN (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt2 (λ x2 x3 . cpw (cfv (cv x1) (cfv (cv x0) cltrn))) (λ x2 x3 . cpw (cfv (cv x1) (cfv (cv x0) cltrn))) (λ x2 x3 . cfv (cin (cfv (cv x2) (cfv (cv x1) (cfv (cv x0) cocaN))) (cfv (cv x3) (cfv (cv x1) (cfv (cv x0) cocaN)))) (cfv (cv x1) (cfv (cv x0) cocaN)))))).

Assume H2: wceq cdib (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt (λ x2 . cdm (cfv (cv x1) (cfv (cv x0) cdia))) (λ x2 . cxp (cfv (cv x2) (cfv (cv x1) (cfv (cv x0) cdia))) (csn (cmpt (λ x3 . cfv (cv x1) (cfv (cv x0) cltrn)) (λ x3 . cres cid (cfv (cv x0) cbs)))))))).

Assume H3: wceq cdic (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt (λ x2 . crab (λ x3 . wn ...) ...) ...))).

...

■

Proofgold Proof