Apply df_conngr__df_eupth__df_frgr__df_plig__df_grpo__df_gid__df_ginv__df_gdiv__df_ablo__df_vc__df_nv__df_va__df_ba__df_sm__df_0v__df_vs__df_nmcv__df_ims with wceq cablo (crab (λ x0 . wral (λ x1 . wral (λ x2 . wceq (co (cv x1) (cv x2) (cv x0)) (co (cv x2) (cv x1) (cv x0))) (λ x2 . crn (cv x0))) (λ x1 . crn (cv x0))) (λ x0 . cgr)).

Assume H0: wceq cconngr (cab (λ x0 . wsbc (λ x1 . wral (λ x2 . wral (λ x3 . wex (λ x4 . wex (λ x5 . wbr (cv x4) (cv x5) (co (cv x2) (cv x3) (cfv (cv x0) cpthson))))) (λ x3 . cv x1)) (λ x2 . cv x1)) (cfv (cv x0) cvtx))).

Assume H1: wceq ceupth (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wbr (cv x1) (cv x2) (cfv (cv x0) ctrls)) (wfo (co cc0 (cfv (cv x1) chash) cfzo) (cdm (cfv (cv x0) ciedg)) (cv x1))))).

Assume H2: wceq cfrgr (cab (λ x0 . wa (wcel (cv x0) cusgr) (wsbc (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wreu (λ x5 . wss (cpr (cpr (cv x5) (cv x3)) (cpr (cv x5) (cv x4))) (cv x2)) (λ x5 . cv x1)) (λ x4 . cdif (cv x1) (csn (cv x3)))) (λ x3 . cv x1)) (cfv (cv x0) cedg)) (cfv (cv x0) cvtx)))).

Assume H3: wceq cplig (cab (λ x0 . w3a (wral (λ x1 . wral (λ x2 . wne (cv x1) (cv x2) ⟶ wreu (λ x3 . wa (wcel (cv x1) (cv x3)) (wcel (cv x2) (cv x3))) (λ x3 . cv x0)) (λ x2 . cuni (cv x0))) (λ x1 . cuni (cv x0))) (wral (λ x1 . wrex (λ x2 . wrex (λ x3 . w3a (wne (cv x2) (cv x3)) (wcel (cv x2) (cv x1)) (wcel (cv x3) (cv x1))) (λ x3 . cuni (cv x0))) (λ x2 . cuni (cv x0))) (λ x1 . cv x0)) (wrex (λ x1 . wrex (λ x2 . wrex (λ x3 . wral (λ x4 . wn (w3a (wcel (cv x1) (cv x4)) (wcel (cv x2) (cv x4)) (wcel (cv ...) ...))) ...) ...) ...) ...))).

...

■

Proofgold Proof