Apply df_cnp__df_lm__df_t0__df_t1__df_haus__df_reg__df_nrm__df_cnrm__df_pnrm__df_cmp__df_conn__df_1stc__df_2ndc__df_lly__df_nlly__df_ref__df_ptfin__df_locfin with ∀ x0 : ι → ο . wceq (cnlly x0) (crab (λ x1 . wral (λ x2 . wral (λ x3 . wrex (λ x4 . wcel (co (cv x1) (cv x4) crest) x0) (λ x4 . cin (cfv (csn (cv x3)) (cfv (cv x1) cnei)) (cpw (cv x2)))) (λ x3 . cv x2)) (λ x2 . cv x1)) (λ x1 . ctop)).

Assume H0: wceq ccnp (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . cmpt (λ x2 . cuni (cv x0)) (λ x2 . crab (λ x3 . wral (λ x4 . wcel (cfv (cv x2) (cv x3)) (cv x4) ⟶ wrex (λ x5 . wa (wcel (cv x2) (cv x5)) (wss (cima (cv x3) (cv x5)) (cv x4))) (λ x5 . cv x0)) (λ x4 . cv x1)) (λ x3 . co (cuni (cv x1)) (cuni (cv x0)) cmap)))).

Assume H1: wceq clm (cmpt (λ x0 . ctop) (λ x0 . copab (λ x1 x2 . w3a (wcel (cv x1) (co (cuni (cv x0)) cc cpm)) (wcel (cv x2) (cuni (cv x0))) (wral (λ x3 . wcel (cv x2) (cv x3) ⟶ wrex (λ x4 . wf (cv x4) (cv x3) (cres (cv x1) (cv x4))) (λ x4 . crn cuz)) (λ x3 . cv x0))))).

Assume H2: wceq ct0 (crab (λ x0 . wral (λ x1 . wral (λ x2 . wral (λ x3 . wb (wcel (cv x1) (cv x3)) (wcel (cv x2) (cv x3))) (λ x3 . cv x0) ⟶ wceq (cv x1) (cv x2)) (λ x2 . cuni (cv x0))) (λ x1 . cuni (cv x0))) (λ x0 . ctop)).

Assume H3: wceq ct1 (crab (λ x0 . wral (λ x1 . wcel (csn (cv x1)) (cfv (cv x0) ccld)) (λ x1 . cuni (cv x0))) (λ x0 . ctop)).

Assume H4: wceq cha (crab (λ x0 . wral (λ x1 . wral (λ x2 . wne (cv x1) (cv x2) ⟶ wrex (λ x3 . wrex (λ x4 . w3a (wcel (cv x1) (cv x3)) (wcel (cv x2) (cv x4)) (wceq (cin (cv x3) (cv x4)) c0)) (λ x4 . cv x0)) (λ x3 . cv x0)) (λ x2 . cuni ...)) ...) ...).

...

■

Proofgold Proof