fact: Fixpoint iperm {M : altMonad} {A : UU0} (s : seq A) : M (seq A) := if s isn't h :: t then Ret [::] else iperm t >>= insert h.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)