Apply df_mpl__df_ltbag__df_opsr__df_evls__df_evl__df_mhp__df_psd__df_selv__df_algind__df_psr1__df_vr1__df_ply1__df_coe1__df_toply1__df_evls1__df_evl1__df_psmet__df_xmet with wceq ctp1 (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . co cn0 c1o cmap) (λ x1 . cfv (cfv c0 (cv x1)) (cv x0)))).

Assume H0: wceq cmpl (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (co (cv x0) (cv x1) cmps) (λ x2 . co (cv x2) (crab (λ x3 . wbr (cv x3) (cfv (cv x1) c0g) cfsupp) (λ x3 . cfv (cv x2) cbs)) cress))).

Assume H1: wceq cltb (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . copab (λ x2 x3 . wa (wss (cpr (cv x2) (cv x3)) (crab (λ x4 . wcel (cima (ccnv (cv x4)) cn) cfn) (λ x4 . co cn0 (cv x1) cmap))) (wrex (λ x4 . wa (wbr (cfv (cv x4) (cv x2)) (cfv (cv x4) (cv x3)) clt) (wral (λ x5 . wbr (cv x4) (cv x5) (cv x0) ⟶ wceq (cfv (cv x5) (cv x2)) (cfv (cv x5) (cv x3))) (λ x5 . cv x1))) (λ x4 . cv x1))))).

Assume H2: wceq copws (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cpw (cxp (cv x0) (cv x0))) (λ x2 . csb (co (cv x0) (cv x1) cmps) (λ x3 . co (cv x3) (cop (cfv cnx cple) (copab (λ x4 x5 . wa (wss (cpr (cv x4) (cv x5)) (cfv (cv x3) cbs)) (wo (wsbc (λ x6 . wrex (λ x7 . wa (wbr (cfv (cv x7) (cv x4)) (cfv (cv x7) (cv x5)) (cfv (cv x1) cplt)) (wral (λ x8 . wbr (cv x8) (cv x7) (co (cv x2) (cv x0) cltb) ⟶ wceq (cfv (cv x8) (cv x4)) (cfv (cv x8) (cv x5))) (λ x8 . cv x6))) (λ x7 . cv x6)) (crab (λ x6 . wcel (cima (ccnv (cv x6)) cn) cfn) (λ x6 . co cn0 (cv x0) cmap))) (wceq (cv x4) (cv x5)))))) csts)))).

Assume H3: wceq ces (cmpt2 ... ... ...).

...

■

Proofgold Proof