proposition: Lemma decr_size_select : bassert_size select.
proof: Proof. case => [|h t]; first by rewrite !selectE fmap_fail /bassert bindfailf. rewrite /bassert selectE bind_fmap fmapE; bind_ext => -[x y] /=. by case: assertPn => //=; rewrite size_tuple /= ltnS leqnn. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)