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 wceq crngiso (cmpt2 (λ x0 x1 . crngo) (λ x0 x1 . crngo) (λ x0 x1 . crab (λ x2 . wf1o (crn (cfv (cv x0) c1st)) (crn (cfv (cv x1) c1st)) (cv x2)) (λ x2 . co (cv x0) (cv x1) crnghom))).

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 ...))))).

...

■

Proofgold Proof