Apply df_ssb_b__df_bj_rnf__df_bj_sngl__df_bj_tag__df_bj_proj__df_bj_1upl__df_bj_pr1__df_bj_2upl__df_bj_pr2__df_elwise__df_bj_moore__df_bj_mpt3__df_bj_sethom__df_bj_tophom__df_bj_mgmhom__df_bj_topmgmhom__df_bj_cur__df_bj_unc with wceq ctophom (cmpt2 (λ x0 x1 . ctps) (λ x0 x1 . ctps) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wcel (cima (ccnv (cv x2)) (cv x3)) (cfv (cv x0) ctopn)) (λ x3 . cfv (cv x1) ctopn)) (λ x2 . co (cfv (cv x0) cbs) (cfv (cv x1) cbs) csethom))).

Assume H0: ∀ x0 : ι → ο . ∀ x1 . wb (wssb (λ x2 . x0 x2) x1) (∀ x2 . wceq (cv x2) (cv x1) ⟶ ∀ x3 . wceq (cv x3) (cv x2) ⟶ x0 x3).

Assume H1: ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . wb (wrnf (λ x2 . x0 x2) (λ x2 . x1 x2)) (wrex (λ x2 . x0 x2) (λ x2 . x1 x2) ⟶ wral (λ x2 . x0 x2) (λ x2 . x1 x2)).

Assume H2: ∀ x0 : ι → ο . wceq (bj_csngl x0) (cab (λ x1 . wrex (λ x2 . wceq (cv x1) (csn (cv x2))) (λ x2 . x0))).

Assume H3: ∀ x0 : ι → ο . wceq (bj_ctag x0) (cun (bj_csngl x0) (csn c0)).

Assume H4: ∀ x0 x1 : ι → ο . wceq (bj_cproj x0 x1) (cab (λ x2 . wcel (csn (cv x2)) (cima x1 (csn x0)))).

Assume H5: ∀ x0 : ι → ο . wceq (bj_c1upl x0) (cxp (csn c0) (bj_ctag x0)).

Assume H6: ∀ x0 : ι → ο . wceq (bj_cpr1 x0) (bj_cproj c0 x0).

Assume H7: ∀ x0 x1 : ι → ο . wceq (bj_c2uple x0 x1) (cun (bj_c1upl x0) (cxp (csn c1o) (bj_ctag x1))).

Assume H8: ∀ x0 : ι → ο . wceq (bj_cpr2 x0) (bj_cproj c1o x0).

Assume H9: wceq celwise (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cab (λ x3 . wrex (λ x4 . wrex (λ x5 . wceq (cv x3) (co (cv x4) (cv x5) (cv x0))) (λ x5 . cv x2)) (λ x4 . cv x1))))).

Assume H10: wceq cmoore (cab (λ x0 . wral (λ x1 . wcel (cin (cuni (cv x0)) (cint (cv x1))) (cv x0)) (λ x1 . cpw (cv x0)))).

Assume H11: ∀ x0 x1 x2 x3 : ι → ι → ι → ι → ο . ∀ x4 x5 . wceq (cmpt3 (λ x6 x7 x8 . x0 x6 x7 x8) (λ x6 x7 x8 . x1 x6 x7 x8) (λ x6 x7 x8 . x2 x6 x7 x8) (λ x6 x7 x8 . x3 x6 x7 x8)) (copab (λ x6 x7 . wrex (λ x8 . wrex (λ x9 . wrex (λ x10 . ...) ...) ...) ...)).

...

■

Proofgold Proof