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