Apply df_supp__df_tpos__df_cur__df_unc__df_undef__df_wrecs__df_smo__df_recs__df_rdg__df_seqom__df_1o__df_2o__df_3o__df_4o__df_oadd__df_omul__df_oexp__df_er with wceq comu (cmpt2 (λ x0 x1 . con0) (λ x0 x1 . con0) (λ x0 x1 . cfv (cv x1) (crdg (cmpt (λ x2 . cvv) (λ x2 . co (cv x2) (cv x0) coa)) c0))).

Assume H0: wceq csupp (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wne (cima (cv x0) (csn (cv x2))) (csn (cv x1))) (λ x2 . cdm (cv x0)))).

Assume H1: ∀ x0 : ι → ο . wceq (ctpos x0) (ccom x0 (cmpt (λ x1 . cun (ccnv (cdm x0)) (csn c0)) (λ x1 . cuni (ccnv (csn (cv x1)))))).

Assume H2: ∀ x0 : ι → ο . wceq (ccur x0) (cmpt (λ x1 . cdm (cdm x0)) (λ x1 . copab (λ x2 x3 . wbr (cop (cv x1) (cv x2)) (cv x3) x0))).

Assume H3: ∀ x0 : ι → ο . wceq (cunc x0) (coprab (λ x1 x2 x3 . wbr (cv x2) (cv x3) (cfv (cv x1) x0))).

Assume H4: wceq cund (cmpt (λ x0 . cvv) (λ x0 . cpw (cuni (cv x0)))).

Assume H5: ∀ x0 x1 x2 : ι → ο . wceq (cwrecs x0 x1 x2) (cuni (cab (λ x3 . wex (λ x4 . w3a (wfn (cv x3) (cv x4)) (wa (wss (cv x4) x0) (wral (λ x5 . wss (cpred x0 x1 (cv x5)) (cv x4)) (λ x5 . cv x4))) (wral (λ x5 . wceq (cfv (cv x5) (cv x3)) (cfv (cres (cv x3) (cpred x0 x1 (cv x5))) x2)) (λ x5 . cv x4)))))).

Assume H6: ∀ x0 : ι → ο . wb (wsmo x0) (w3a (wf (cdm x0) con0 x0) (word (cdm x0)) (wral (λ x1 . wral (λ x2 . wcel (cv x1) (cv x2) ⟶ wcel (cfv (cv x1) x0) (cfv (cv x2) x0)) (λ x2 . cdm x0)) (λ x1 . cdm x0))).

Assume H7: ∀ x0 : ι → ο . wceq (crecs x0) (cwrecs con0 cep x0).

Assume H8: ∀ x0 x1 : ι → ο . wceq (crdg x0 x1) (crecs (cmpt (λ x2 . cvv) (λ x2 . cif (wceq (cv x2) c0) x1 (cif (wlim (cdm (cv x2))) (cuni (crn (cv x2))) (cfv (cfv (cuni (cdm (cv x2))) (cv x2)) ...))))).

...

■

Proofgold Proof