Apply df_salgen__df_sumge0__df_mea__df_ome__df_caragen__df_ovoln__df_voln__df_smblfn__df_dfat__df_afv__df_aov__df_nelbr__df_iccp__df_pfx__df_fmtno__df_even__df_odd__df_gbe with wceq cpfx (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cn0) (λ x0 x1 . co (cv x0) (cop cc0 (cv x1)) csubstr)).

Assume H0: wceq csalgen (cmpt (λ x0 . cvv) (λ x0 . cint (crab (λ x1 . wa (wceq (cuni (cv x1)) (cuni (cv x0))) (wss (cv x0) (cv x1))) (λ x1 . csalg)))).

Assume H1: wceq csumge0 (cmpt (λ x0 . cvv) (λ x0 . cif (wcel cpnf (crn (cv x0))) cpnf (csup (crn (cmpt (λ x1 . cin (cpw (cdm (cv x0))) cfn) (λ x1 . csu (cv x1) (λ x2 . cfv (cv x2) (cv x0))))) cxr clt))).

Assume H2: wceq cmea (cab (λ x0 . wa (wa (wa (wf (cdm (cv x0)) (co cc0 cpnf cicc) (cv x0)) (wcel (cdm (cv x0)) csalg)) (wceq (cfv c0 (cv x0)) cc0)) (wral (λ x1 . wa (wbr (cv x1) com cdom) (wdisj (λ x2 . cv x1) (λ x2 . cv x2)) ⟶ wceq (cfv (cuni (cv x1)) (cv x0)) (cfv (cres (cv x0) (cv x1)) csumge0)) (λ x1 . cpw (cdm (cv x0)))))).

Assume H3: wceq come (cab (λ x0 . wa (wa (wa (wa (wf (cdm (cv x0)) (co cc0 cpnf cicc) (cv x0)) (wceq (cdm (cv x0)) (cpw (cuni (cdm (cv x0)))))) (wceq (cfv c0 (cv x0)) cc0)) (wral (λ x1 . wral (λ x2 . wbr (cfv (cv x2) (cv x0)) (cfv (cv x1) (cv x0)) cle) (λ x2 . cpw (cv x1))) (λ x1 . cpw (cuni (cdm (cv x0)))))) (wral (λ x1 . wbr (cv x1) com cdom ⟶ wbr (cfv (cuni (cv x1)) (cv x0)) (cfv (cres (cv x0) (cv x1)) csumge0) cle) (λ x1 . cpw (cdm (cv x0)))))).

Assume H4: wceq ccaragen (cmpt (λ x0 . come) (λ x0 . crab (λ x1 . wral (λ x2 . wceq (co (cfv (cin (cv x2) (cv x1)) (cv x0)) (cfv (cdif (cv x2) (cv x1)) ...) ...) ...) ...) ...)).

...

■

Proofgold Proof