Apply df_msub__df_mvh__df_mpst__df_msr__df_msta__df_mfs__df_mcls__df_mpps__df_mthm__df_m0s__df_msa__df_mwgfs__df_msyn__df_mtree__df_mst__df_msax__df_mufs__df_muv with wceq cmsax (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cmsa) (λ x1 . cima (cfv (cv x0) cmvh) (cfv (cv x1) (cfv (cv x0) cmvrs))))).

Assume H0: wceq cmsub (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . co (cfv (cv x0) cmrex) (cfv (cv x0) cmvar) cpm) (λ x1 . cmpt (λ x2 . cfv (cv x0) cmex) (λ x2 . cop (cfv (cv x2) c1st) (cfv (cfv (cv x2) c2nd) (cfv (cv x1) (cfv (cv x0) cmrsub))))))).

Assume H1: wceq cmvh (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cmvar) (λ x1 . cop (cfv (cv x1) (cfv (cv x0) cmty)) (cs1 (cv x1))))).

Assume H2: wceq cmpst (cmpt (λ x0 . cvv) (λ x0 . cxp (cxp (crab (λ x1 . wceq (ccnv (cv x1)) (cv x1)) (λ x1 . cpw (cfv (cv x0) cmdv))) (cin (cpw (cfv (cv x0) cmex)) cfn)) (cfv (cv x0) cmex))).

Assume H3: wceq cmsr (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cmpst) (λ x1 . csb (cfv (cfv (cv x1) c1st) c2nd) (λ x2 . csb (cfv (cv x1) c2nd) (λ x3 . cotp (cin (cfv (cfv (cv x1) c1st) c1st) (csb (cuni (cima (cfv (cv x0) cmvrs) (cun (cv x2) (csn (cv x3))))) (λ x4 . cxp (cv x4) (cv x4)))) (cv x2) (cv x3)))))).

Assume H4: wceq cmsta (cmpt (λ x0 . cvv) (λ x0 . crn (cfv (cv x0) cmsr))).

Assume H5: wceq cmfs (cab (λ x0 . wa (wa (wceq (cin (cfv (cv x0) cmcn) (cfv (cv x0) cmvar)) c0) (wf (cfv (cv x0) cmvar) (cfv (cv x0) cmtc) (cfv (cv x0) cmty))) (wa (wss (cfv (cv x0) cmax) (cfv (cv x0) cmsta)) (wral (λ x1 . wn (wcel (cima (ccnv (cfv (cv x0) cmty)) (csn (cv x1))) cfn)) ...)))).

...

■

Proofgold Proof