Apply df_cph__df_tch__df_cfil__df_cau__df_cmet__df_cms__df_bn__df_hl__df_rrx__df_ehl__df_ovol__df_vol__df_mbf__df_itg1__df_itg2__df_ibl__df_itg__df_0p with wceq ctch (cmpt (λ x0 . cvv) (λ x0 . co (cv x0) (cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . cfv (co (cv x1) (cv x1) (cfv (cv x0) cip)) csqrt)) ctng)).

Assume H0: wceq ccph (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . w3a (wceq (cv x1) (co ccnfld (cv x2) cress)) (wss (cima csqrt (cin (cv x2) (co cc0 cpnf cico))) (cv x2)) (wceq (cfv (cv x0) cnm) (cmpt (λ x3 . cfv (cv x0) cbs) (λ x3 . cfv (co (cv x3) (cv x3) (cfv (cv x0) cip)) csqrt)))) (cfv (cv x1) cbs)) (cfv (cv x0) csca)) (λ x0 . cin cphl cnlm)).

Assume H1: wceq ctch (cmpt (λ x0 . cvv) (λ x0 . co (cv x0) (cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . cfv (co (cv x1) (cv x1) (cfv (cv x0) cip)) csqrt)) ctng)).

Assume H2: wceq ccfil (cmpt (λ x0 . cuni (crn cxmt)) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wss (cima (cv x0) (cxp (cv x3) (cv x3))) (co cc0 (cv x2) cico)) (λ x3 . cv x1)) (λ x2 . crp)) (λ x1 . cfv (cdm (cdm (cv x0))) cfil))).

Assume H3: wceq cca (cmpt (λ x0 . cuni (crn cxmt)) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wf (cfv (cv x3) cuz) (co (cfv (cv x3) (cv x1)) (cv x2) (cfv (cv x0) cbl)) (cres (cv x1) (cfv (cv x3) cuz))) (λ x3 . cz)) (λ x2 . crp)) (λ x1 . co (cdm (cdm (cv x0))) cc cpm))).

Assume H4: wceq cms (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wne (co (cfv (cv x1) cmopn) (cv x2) cflim) c0) (λ x2 . cfv (cv x1) ccfil)) (λ x1 . cfv (cv x0) cme))).

Assume H5: wceq ccms (crab (λ x0 . wsbc (λ x1 . wcel (cres ... ...) ...) ...) ...).

...

■

Proofgold Proof