Apply df_rag__df_perpg__df_hpg__df_mid__df_lmi__df_cgra__df_inag__df_leag__df_eqlg__df_ttg__df_ee__df_btwn__df_cgr__df_eeng__df_edgf__df_vtx__df_iedg__df_edg with wceq cvtx (cmpt (λ x0 . cvv) (λ x0 . cif (wcel (cv x0) (cxp cvv cvv)) (cfv (cv x0) c1st) (cfv (cv x0) cbs))).

Assume H0: wceq crag (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wa (wceq (cfv (cv x1) chash) c3) (wceq (co (cfv cc0 (cv x1)) (cfv c2 (cv x1)) (cfv (cv x0) cds)) (co (cfv cc0 (cv x1)) (cfv (cfv c2 (cv x1)) (cfv (cfv c1 (cv x1)) (cfv (cv x0) cmir))) (cfv (cv x0) cds)))) (λ x1 . cword (cfv (cv x0) cbs)))).

Assume H1: wceq cperpg (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wa (wcel (cv x1) (crn (cfv (cv x0) clng))) (wcel (cv x2) (crn (cfv (cv x0) clng)))) (wrex (λ x3 . wral (λ x4 . wral (λ x5 . wcel (cs3 (cv x4) (cv x3) (cv x5)) (cfv (cv x0) crag)) (λ x5 . cv x2)) (λ x4 . cv x1)) (λ x3 . cin (cv x1) (cv x2)))))).

Assume H2: wceq chpg (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . crn (cfv (cv x0) clng)) (λ x1 . copab (λ x2 x3 . wsbc (λ x4 . wsbc (λ x5 . wrex (λ x6 . wa (wa (wa (wcel (cv x2) (cdif (cv x4) (cv x1))) (wcel (cv x6) (cdif (cv x4) (cv x1)))) (wrex (λ x7 . wcel (cv x7) (co (cv x2) (cv x6) (cv x5))) (λ x7 . cv x1))) (wa (wa (wcel (cv x3) (cdif (cv x4) (cv x1))) (wcel (cv x6) (cdif (cv x4) (cv x1)))) (wrex (λ x7 . wcel (cv x7) (co (cv x3) (cv x6) (cv x5))) (λ x7 . cv x1)))) (λ x6 . cv x4)) (cfv (cv x0) citv)) (cfv (cv x0) cbs))))).

Assume H3: wceq cmid (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv ... ...) ...)).

...

■

Proofgold Proof