proposition: Lemma arbitrary_flatten (A : UU0) def (s : seq A) (f : A -> A) : (0 < size s)%nat -> (do x <- arbitrary def s; Ret (f x))%Do = arbitrary def (flatten [seq [:: f y] | y <- s]) :> M _.
proof: Proof. elim: s f => // a [_ f _ /=|h t ih f _]. by rewrite /arbitrary /= bindretf. rewrite [h :: t]lock /= -lock [in RHS]arbitrary_cons// -ih//. by rewrite arbitrary_cons// alt_bindDl bindretf. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)