Apply df_sx__df_meas__df_dde__df_ae__df_fae__df_mbfm__df_oms__df_carsg__df_sitg__df_sitm__df_itgm__df_sseq__df_fib__df_prob__df_cndprob__df_rrv__df_orvc__df_repr with wceq csx (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cfv (crn (cmpt2 (λ x2 x3 . cv x0) (λ x2 x3 . cv x1) (λ x2 x3 . cxp (cv x2) (cv x3)))) csigagen)).

Assume H0: wceq csx (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cfv (crn (cmpt2 (λ x2 x3 . cv x0) (λ x2 x3 . cv x1) (λ x2 x3 . cxp (cv x2) (cv x3)))) csigagen)).

Assume H1: wceq cmeas (cmpt (λ x0 . cuni (crn csiga)) (λ x0 . cab (λ x1 . w3a (wf (cv x0) (co cc0 cpnf cicc) (cv x1)) (wceq (cfv c0 (cv x1)) cc0) (wral (λ x2 . wa (wbr (cv x2) com cdom) (wdisj (λ x3 . cv x2) (λ x3 . cv x3)) ⟶ wceq (cfv (cuni (cv x2)) (cv x1)) (cesum (λ x3 . cv x2) (λ x3 . cfv (cv x3) (cv x1)))) (λ x2 . cpw (cv x0)))))).

Assume H2: wceq cdde (cmpt (λ x0 . cpw cr) (λ x0 . cif (wcel cc0 (cv x0)) c1 cc0)).

Assume H3: wceq cae (copab (λ x0 x1 . wceq (cfv (cdif (cuni (cdm (cv x1))) (cv x0)) (cv x1)) cc0)).

Assume H4: wceq cfae (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cuni (crn cmeas)) (λ x0 x1 . copab (λ x2 x3 . wa (wa (wcel (cv x2) (co (cdm (cv x0)) (cuni (cdm (cv x1))) cmap)) (wcel (cv x3) (co (cdm (cv x0)) (cuni (cdm (cv x1))) cmap))) (wbr (crab (λ x4 . wbr (cfv (cv x4) (cv x2)) (cfv (cv x4) (cv x3)) (cv x0)) (λ x4 . cuni (cdm (cv x1)))) (cv x1) cae)))).

Assume H5: wceq cmbfm (cmpt2 (λ x0 x1 . cuni (crn csiga)) (λ x0 x1 . cuni (crn csiga)) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wcel (cima (ccnv (cv x2)) (cv x3)) (cv x0)) (λ x3 . cv x1)) (λ x2 . co (cuni (cv x1)) (cuni (cv x0)) cmap))).

Assume H6: wceq coms (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw ...) ...)).

...

■

Proofgold Proof