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 cfusgr (crab (λ x0 . wcel (cfv (cv x0) cvtx) cfn) (λ x0 . cusgr)).

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 . w3a (wss (cfv (cv x0) cvtx) (cfv (cv x1) cvtx)) (wceq (cfv (cv x0) ciedg) (cres (cfv (cv x1) ciedg) (cdm (cfv (cv x0) ciedg)))) ...)).

...

■

Proofgold Proof