Apply df_nrg__df_nlm__df_nvc__df_nmo__df_nghm__df_nmhm__df_ii__df_cncf__df_htpy__df_phtpy__df_phtpc__df_pco__df_om1__df_omn__df_pi1__df_pin__df_clm__df_cvs with wceq cpi1 (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . cuni (cv x0)) (λ x0 x1 . co (co (cv x0) (cv x1) comi) (cfv (cv x0) cphtpc) cqus)).

Assume H0: wceq cnrg (crab (λ x0 . wcel (cfv (cv x0) cnm) (cfv (cv x0) cabv)) (λ x0 . cngp)).

Assume H1: wceq cnlm (crab (λ x0 . wsbc (λ x1 . wa (wcel (cv x1) cnrg) (wral (λ x2 . wral (λ x3 . wceq (cfv (co (cv x2) (cv x3) (cfv (cv x0) cvsca)) (cfv (cv x0) cnm)) (co (cfv (cv x2) (cfv (cv x1) cnm)) (cfv (cv x3) (cfv (cv x0) cnm)) cmul)) (λ x3 . cfv (cv x0) cbs)) (λ x2 . cfv (cv x1) cbs))) (cfv (cv x0) csca)) (λ x0 . cin cngp clmod)).

Assume H2: wceq cnvc (cin cnlm clvec).

Assume H3: wceq cnmo (cmpt2 (λ x0 x1 . cngp) (λ x0 x1 . cngp) (λ x0 x1 . cmpt (λ x2 . co (cv x0) (cv x1) cghm) (λ x2 . cinf (crab (λ x3 . wral (λ x4 . wbr (cfv (cfv (cv x4) (cv x2)) (cfv (cv x1) cnm)) (co (cv x3) (cfv (cv x4) (cfv (cv x0) cnm)) cmul) cle) (λ x4 . cfv (cv x0) cbs)) (λ x3 . co cc0 cpnf cico)) cxr clt))).

Assume H4: wceq cnghm (cmpt2 (λ x0 x1 . cngp) (λ x0 x1 . cngp) (λ x0 x1 . cima (ccnv (co (cv x0) (cv x1) cnmo)) cr)).

Assume H5: wceq cnmhm (cmpt2 (λ x0 x1 . cnlm) (λ x0 x1 . cnlm) (λ x0 x1 . cin (co (cv x0) (cv x1) clmhm) (co (cv x0) (cv x1) cnghm))).

Assume H6: wceq cii (cfv (cres (ccom cabs cmin) (cxp (co cc0 c1 cicc) (co cc0 c1 cicc))) cmopn).

Assume H7: wceq ccncf (cmpt2 (λ x0 x1 . cpw cc) (λ x0 x1 . cpw cc) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wrex (λ x5 . wral (λ x6 . ... ⟶ wbr (cfv (co (cfv (cv x3) (cv x2)) (cfv (cv x6) ...) ...) ...) ... ...) ...) ...) ...) ...) ...)).

...

■

Proofgold Proof