Apply df_uhgr__df_ushgr__df_upgr__df_umgr__df_uspgr__df_usgr__df_subgr__df_fusgr__df_nbgr__df_uvtx__df_cplgr__df_cusgr__df_vtxdg__df_rgr__df_rusgr__df_ewlks__df_wlks__df_wlkson with wceq cnbgr (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cfv (cv x0) cvtx) (λ x0 x1 . crab (λ x2 . wrex (λ x3 . wss (cpr (cv x1) (cv x2)) (cv x3)) (λ x3 . cfv (cv x0) cedg)) (λ x2 . cdif (cfv (cv x0) cvtx) (csn (cv x1))))).

Assume H0: wceq cuhgr (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wf (cdm (cv x2)) (cdif (cpw (cv x1)) (csn c0)) (cv x2)) (cfv (cv x0) ciedg)) (cfv (cv x0) cvtx))).

Assume H1: wceq cushgr (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wf1 (cdm (cv x2)) (cdif (cpw (cv x1)) (csn c0)) (cv x2)) (cfv (cv x0) ciedg)) (cfv (cv x0) cvtx))).

Assume H2: wceq cupgr (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wf (cdm (cv x2)) (crab (λ x3 . wbr (cfv (cv x3) chash) c2 cle) (λ x3 . cdif (cpw (cv x1)) (csn c0))) (cv x2)) (cfv (cv x0) ciedg)) (cfv (cv x0) cvtx))).

Assume H3: wceq cumgr (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wf (cdm (cv x2)) (crab (λ x3 . wceq (cfv (cv x3) chash) c2) (λ x3 . cdif (cpw (cv x1)) (csn c0))) (cv x2)) (cfv (cv x0) ciedg)) (cfv (cv x0) cvtx))).

Assume H4: wceq cuspgr (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wf1 (cdm (cv x2)) (crab (λ x3 . wbr (cfv (cv x3) chash) c2 cle) (λ x3 . cdif (cpw (cv x1)) (csn c0))) (cv x2)) (cfv (cv x0) ciedg)) (cfv (cv x0) cvtx))).

Assume H5: wceq cusgr (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wf1 (cdm (cv x2)) (crab (λ x3 . wceq (cfv (cv x3) chash) c2) (λ x3 . cdif (cpw (cv x1)) (csn c0))) (cv x2)) (cfv (cv x0) ciedg)) (cfv (cv x0) cvtx))).

Assume H6: wceq csubgr (copab (λ x0 x1 . ...)).

...

■

Proofgold Proof