Apply df_sslt__df_scut__df_made__df_old__df_new__df_left__df_right__df_txp__df_pprod__df_sset__df_trans__df_bigcup__df_fix__df_limits__df_funs__df_singleton__df_singles__df_image with ∀ x0 x1 : ι → ο . wceq (cpprod x0 x1) (ctxp (ccom x0 (cres c1st (cxp cvv cvv))) (ccom x1 (cres c2nd (cxp cvv cvv)))).

Assume H0: wceq csslt (copab (λ x0 x1 . w3a (wss (cv x0) csur) (wss (cv x1) csur) (wral (λ x2 . wral (λ x3 . wbr (cv x2) (cv x3) cslt) (λ x3 . cv x1)) (λ x2 . cv x0)))).

Assume H1: wceq cscut (cmpt2 (λ x0 x1 . cpw csur) (λ x0 x1 . cima csslt (csn (cv x0))) (λ x0 x1 . crio (λ x2 . wceq (cfv (cv x2) cbday) (cint (cima cbday (crab (λ x3 . wa (wbr (cv x0) (csn (cv x3)) csslt) (wbr (csn (cv x3)) (cv x1) csslt)) (λ x3 . csur))))) (λ x2 . crab (λ x3 . wa (wbr (cv x0) (csn (cv x3)) csslt) (wbr (csn (cv x3)) (cv x1) csslt)) (λ x3 . csur)))).

Assume H2: wceq cmade (crecs (cmpt (λ x0 . cvv) (λ x0 . cima cscut (cxp (cpw (cuni (crn (cv x0)))) (cpw (cuni (crn (cv x0)))))))).

Assume H3: wceq cold (cmpt (λ x0 . con0) (λ x0 . cuni (cima cmade (cv x0)))).

Assume H4: wceq cnew (cmpt (λ x0 . con0) (λ x0 . cdif (cfv (cv x0) cold) (cfv (cv x0) cmade))).

Assume H5: wceq cleft (cmpt (λ x0 . csur) (λ x0 . crab (λ x1 . wral (λ x2 . wa (wbr (cv x1) (cv x2) cslt) (wbr (cv x2) (cv x0) cslt) ⟶ wcel (cfv (cv x1) cbday) (cfv (cv x2) cbday)) (λ x2 . csur)) (λ x1 . cfv (cfv (cv x0) cbday) cold))).

Assume H6: wceq cright (cmpt (λ x0 . csur) (λ x0 . crab (λ x1 . wral (λ x2 . wa (wbr (cv x0) (cv x2) cslt) (wbr (cv x2) (cv x1) cslt) ⟶ wcel (cfv (cv x1) cbday) (cfv (cv x2) cbday)) (λ x2 . csur)) (λ x1 . cfv (cfv (cv x0) cbday) cold))).

Assume H7: ∀ x0 x1 : ι → ο . wceq (ctxp x0 x1) (cin (ccom (ccnv ...) ...) ...).

...

■

Proofgold Proof