proposition: Lemma insert_isNondet A (s : seq A) a : plus_isNondet (@insert M _ a s).
proof: Proof. elim: s => /= [|h t ih]; first by exists (ndRet [:: a]). rewrite insertE /=; have [syn synE] := ih. exists (ndAlt (ndRet [:: a, h & t]) (ndBind syn (fun x => ndRet (h :: x)))). by rewrite /= synE fmapE. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)