proposition: Lemma lemma31 b : foldl op b (o) iperm = Ret \o foldl op b :> (_ -> M _).
proof: Proof. rewrite boolp.funeqE => xs; move: xs b; elim => [/=|x xs IH] b. by rewrite fcompE fmapE bindretf. rewrite fcompE fmap_bind. have opP' : forall (x y : A) (w : seq A), (foldl op b w (.) x) (.) y = (foldl op b w (.) y) (.) x. move=> ? ? ?. by rewrite opP. under eq_bind do rewrite (lemma32 M opP'). transitivity ((Ret \o foldl op (b (.) x)) xs : M _); last by []. rewrite -IH. rewrite [in RHS]fcompE. rewrite fmapE. bind_ext => ys. rewrite /= -cats1 foldl_cat /=. congr (Ret _ : M _). elim: ys b opP' => // y ys ih /= b opP'. rewrite ih //=. rewrite -/(foldl op b [::]). by rewrite opP'. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib