Apply df_mfsh__df_mevl__df_mvl__df_mvsb__df_mfrel__df_mdl__df_musyn__df_gmdl__df_mitp__df_mfitp__df_irng__df_cplmet__df_homlimb__df_homlim__df_plfl__df_sfl1__df_sfl__df_psl with wceq cusyn (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cmuv) (λ x1 . cop (cfv (cfv (cv x1) c1st) (cfv (cv x0) cmsy)) (cfv (cv x1) c2nd)))).

Assume H0: wceq cmfsh (cslot c8).

Assume H1: wceq cmevl (cslot c9).

Assume H2: wceq cmvl (cmpt (λ x0 . cvv) (λ x0 . cixp (λ x1 . cfv (cv x0) cmvar) (λ x1 . cima (cfv (cv x0) cmuv) (csn (cfv (cv x1) (cfv (cv x0) cmty)))))).

Assume H3: wceq cmvsb (cmpt (λ x0 . cvv) (λ x0 . coprab (λ x1 x2 x3 . w3a (wa (wcel (cv x1) (crn (cfv (cv x0) cmsub))) (wcel (cv x2) (cfv (cv x0) cmvl))) (wral (λ x4 . wbr (cv x2) (cfv (cfv (cv x4) (cfv (cv x0) cmvh)) (cv x1)) (cdm (cfv (cv x0) cmevl))) (λ x4 . cfv (cv x0) cmvar)) (wceq (cv x3) (cmpt (λ x4 . cfv (cv x0) cmvar) (λ x4 . co (cv x2) (cfv (cfv (cv x4) (cfv (cv x0) cmvh)) (cv x1)) (cfv (cv x0) cmevl))))))).

Assume H4: wceq cmfr (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wa (wceq (ccnv (cv x1)) (cv x1)) (wral (λ x2 . wral (λ x3 . wrex (λ x4 . wss (cv x3) (cima (cv x1) (csn (cv x4)))) (λ x4 . cima (cfv (cv x0) cmuv) (csn (cv x2)))) (λ x3 . cin (cpw (cfv (cv x0) cmuv)) cfn)) (λ x2 . cfv (cv x0) cmvt))) (λ x1 . cpw (cxp (cfv (cv x0) cmuv) (cfv (cv x0) cmuv))))).

Assume H5: wceq cmdl (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wa (w3a (wss (cv x1) (cxp (cfv (cv x0) cmtc) cvv)) (wcel (cv x5) (cfv (cv x0) cmfr)) (wcel (cv x4) (co (cv x1) (cxp (cv x3) (cfv (cv x0) cmex)) cpm))) (wral (λ x6 . wa (w3a ... ... ...) ...) ...)) ...) ...) ...) ...) ...) ...).

...

■

Proofgold Proof