proposition: Lemma tpermsE s : (perms s = if s isn't h :: t then Ret [::] else do x <- tselect (h :: t); do y <- perms x.2; Ret (x.1 :: y))%Do.
proof: Proof. rewrite {1}/perms Init.Wf.Fix_eq //; [by case: s|move=> s' f g H]. by rewrite /perms'; destruct s' => //; bind_ext=> x; rewrite H. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)