proposition: Lemma base_case y : p y -> (unfoldM p select >=> foldr op (Ret [::])) y = Ret [::].
proof: Proof. move=> py. transitivity (Ret [::] >>= foldr op (Ret [::])). rewrite /kleisli bindretf /= join_fmap unfoldME; last exact: decr_size_select. by rewrite py bindretf. by rewrite bindretf. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib