proposition: Lemma queensBodyE : queensBody M = hyloM (@opdot_queens M) [::] (@nilp _) select seed_select (@well_founded_size _).
proof: Proof. rewrite /queensBody boolp.funeqE => -[|h t]. - rewrite /= permsE /= hyloME ?bindretf //; exact: decr_size_select. - by rewrite [h :: t]lock -theorem51 /kleisli /= join_fmap perms_uperm. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib