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 ccur_ (cmpt3 (λ x0 x1 x2 . cvv) (λ x0 x1 x2 . cvv) (λ x0 x1 x2 . cvv) (λ x0 x1 x2 . cmpt (λ x3 . co (cxp (cv x0) (cv x1)) (cv x2) csethom) (λ x3 . cmpt (λ x4 . cv x0) (λ x4 . cmpt (λ x5 . cv x1) (λ x5 . cfv (cop (cv x4) (cv x5)) (cv x3)))))).
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 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 ... ...) ...) ...)).