proposition: Lemma perms_uperm s : perms s = uperm s.
proof: Proof. move Hn : (size s) => n. elim: n s Hn => [|n IH [//|h t] /= [tn]]. case => //; by rewrite permsE upermE. rewrite tpermsE upermE selectE bind_fmap; bind_ext => -[a b]. by rewrite IH // size_tuple. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)