fact: Fixpoint subs (s : seq A) : M (seq A) := if s isn't h :: t then Ret [::] else let t' := subs t in fmap (cons h) t' [~] t'.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)