Apply df_mndo__df_ghomOLD__df_rngo__df_drngo__df_rngohom__df_rngoiso__df_risc__df_com2__df_fld__df_crngo__df_idl__df_pridl__df_maxidl__df_prrngo__df_dmn__df_igen__df_xrn__df_coss with ∀ x0 x1 : ι → ο . wceq (cxrn x0 x1) (cin (ccom (ccnv (cres c1st (cxp cvv cvv))) x0) (ccom (ccnv (cres c2nd (cxp cvv cvv))) x1)).

Assume H0: wceq cmndo (cin csem cexid).

Assume H1: wceq cghomOLD (cmpt2 (λ x0 x1 . cgr) (λ x0 x1 . cgr) (λ x0 x1 . cab (λ x2 . wa (wf (crn (cv x0)) (crn (cv x1)) (cv x2)) (wral (λ x3 . wral (λ x4 . wceq (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) (cv x1)) (cfv (co (cv x3) (cv x4) (cv x0)) (cv x2))) (λ x4 . crn (cv x0))) (λ x3 . crn (cv x0)))))).

Assume H2: wceq crngo (copab (λ x0 x1 . wa (wa (wcel (cv x0) cablo) (wf (cxp (crn (cv x0)) (crn (cv x0))) (crn (cv x0)) (cv x1))) (wa (wral (λ x2 . wral (λ x3 . wral (λ x4 . w3a (wceq (co (co (cv x2) (cv x3) (cv x1)) (cv x4) (cv x1)) (co (cv x2) (co (cv x3) (cv x4) (cv x1)) (cv x1))) (wceq (co (cv x2) (co (cv x3) (cv x4) (cv x0)) (cv x1)) (co (co (cv x2) (cv x3) (cv x1)) (co (cv x2) (cv x4) (cv x1)) (cv x0))) (wceq (co (co (cv x2) (cv x3) (cv x0)) (cv x4) (cv x1)) (co (co (cv x2) (cv x4) (cv x1)) (co (cv x3) (cv x4) (cv x1)) (cv x0)))) (λ x4 . crn (cv x0))) (λ x3 . crn (cv x0))) (λ x2 . crn (cv x0))) (wrex (λ x2 . wral (λ x3 . wa (wceq (co (cv x2) (cv x3) (cv x1)) (cv x3)) (wceq (co (cv x3) (cv x2) (cv x1)) (cv x3))) (λ x3 . crn (cv x0))) (λ x2 . crn (cv x0)))))).

Assume H3: wceq cdrng (copab (λ x0 x1 . wa ... ...)).

...

■

Proofgold Proof