Apply df_sca__df_vsca__df_ip__df_tset__df_ple__df_ocomp__df_ds__df_unif__df_hom__df_cco__df_rest__df_topn__df_0g__df_gsum__df_topgen__df_pt__df_prds__df_pws with wceq ctg (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wss (cv x1) (cuni (cin (cv x0) (cpw (cv x1))))))).

Assume H0: wceq csca (cslot c5).

Assume H1: wceq cvsca (cslot c6).

Assume H2: wceq cip (cslot c8).

Assume H3: wceq cts (cslot c9).

Assume H4: wceq cple (cslot (cdc c1 cc0)).

Assume H5: wceq coc (cslot (cdc c1 c1)).

Assume H6: wceq cds (cslot (cdc c1 c2)).

Assume H7: wceq cunif (cslot (cdc c1 c3)).

Assume H8: wceq chom (cslot (cdc c1 c4)).

Assume H9: wceq cco (cslot (cdc c1 c5)).

Assume H10: wceq crest (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . crn (cmpt (λ x2 . cv x0) (λ x2 . cin (cv x2) (cv x1))))).

Assume H11: wceq ctopn (cmpt (λ x0 . cvv) (λ x0 . co (cfv (cv x0) cts) (cfv (cv x0) cbs) crest)).

Assume H12: wceq c0g (cmpt (λ x0 . cvv) (λ x0 . cio (λ x1 . wa (wcel (cv x1) (cfv (cv x0) cbs)) (wral (λ x2 . wa (wceq (co (cv x1) (cv x2) (cfv (cv x0) cplusg)) (cv x2)) (wceq (co (cv x2) (cv x1) (cfv (cv x0) cplusg)) (cv x2))) (λ x2 . cfv (cv x0) cbs))))).

Assume H13: wceq cgsu (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (crab (λ x2 . wral (λ x3 . wa (wceq (co (cv x2) (cv x3) (cfv (cv x0) cplusg)) (cv x3)) (wceq (co (cv x3) (cv x2) (cfv (cv x0) cplusg)) (cv x3))) (λ x3 . cfv (cv x0) cbs)) (λ x2 . cfv (cv x0) cbs)) (λ x2 . cif (wss (crn (cv x1)) (cv x2)) (cfv (cv x0) c0g) (cif (wcel (cdm (cv x1)) (crn cfz)) (cio (λ x3 . wex (λ x4 . wrex (λ x5 . wa (wceq (cdm (cv x1)) (co (cv x4) (cv x5) cfz)) (wceq (cv x3) (cfv (cv x5) (cseq (cfv (cv ...) ...) ... ...)))) ...))) ...)))).

...

■

Proofgold Proof