proposition: Lemma upermE s : (uperm s = if s isn't h :: t then Ret [::] else do a <- select (h :: t) ; do b <- uperm a.2; Ret (a.1 :: b))%Do.
proof: Proof. rewrite /uperm unfoldME; last exact: decr_size_select. case: s => // h t; rewrite (_ : nilp _ = false) //. by bind_ext => -[x1 x2] ; rewrite fmapE. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)