proposition: Lemma permsE s : (perms s = if s isn't h :: t then Ret [::] else do x <- select (h :: t); do y <- perms x.2; Ret (x.1 :: y))%Do.
proof: Proof. rewrite tpermsE; case: s => // h t. by rewrite selectE bind_fmap. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)