Apply df_gzext__df_gzrep__df_gzpow__df_gzun__df_gzreg__df_gzinf__df_gzf__df_mcn__df_mvar__df_mty__df_mtc__df_mmax__df_mvt__df_mrex__df_mex__df_mdv__df_mvrs__df_mrsub with wceq cmdv (cmpt (λ x0 . cvv) (λ x0 . cdif (cxp (cfv (cv x0) cmvar) (cfv (cv x0) cmvar)) cid)).

Assume H0: wceq cgze (co (cgol (co (co c2o c0 cgoe) (co c2o c1o cgoe) cgob) c2o) (co c0 c1o cgoq) cgoi).

Assume H1: wceq cgzr (cmpt (λ x0 . cfv com cfmla) (λ x0 . co (cgol (cgox (cgol (co (cgol (cv x0) c1o) (co c2o c1o cgoq) cgoi) c2o) c1o) c3o) (cgol (cgol (co (co c2o c1o cgoe) (cgox (co (co c3o c0 cgoe) (cgol (cv x0) c1o) cgoa) c3o) cgob) c2o) c1o) cgoi)).

Assume H2: wceq cgzp (cgox (cgol (co (cgol (co (co c1o c2o cgoe) (co c1o c0 cgoe) cgob) c1o) (co c2o c1o cgoe) cgoi) c2o) c1o).

Assume H3: wceq cgzu (cgox (cgol (co (cgox (co (co c2o c1o cgoe) (co c1o c0 cgoe) cgoa) c1o) (co c2o c1o cgoe) cgoi) c2o) c1o).

Assume H4: wceq cgzg (co (cgox (co c1o c0 cgoe) c1o) (cgox (co (co c1o c0 cgoe) (cgol (co (co c2o c1o cgoe) (cgon (co c2o c0 cgoe)) cgoi) c2o) cgoa) c1o) cgoi).

Assume H5: wceq cgzi (cgox (co (co c0 c1o cgoe) (cgol (co (co c2o c1o cgoe) (cgox (co (co c2o c0 cgoe) (co c0 c1o cgoe) cgoa) c0) cgoi) c2o) cgoa) c1o).

Assume H6: wceq cgzf (cab (λ x0 . w3a (w3a (wtr (cv x0)) (wbr (cv x0) cgze cprv) (wbr (cv x0) cgzp cprv)) (w3a (wbr (cv x0) cgzu cprv) (wbr (cv x0) cgzg cprv) (wbr (cv x0) cgzi cprv)) (wral (λ x1 . wbr (cv x0) (cfv (cv x1) cgzr) cprv) (λ x1 . cfv com cfmla)))).

Assume H7: wceq cmcn (cslot ...).

...

■

Proofgold Proof