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 : ι → ο . wceq (ccoss x0) (copab (λ x1 x2 . wex (λ x3 . wa (wbr (cv x3) (cv x1) x0) (wbr (cv x3) (cv x2) x0)))).

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

...

■

Proofgold Proof