proposition: Lemma mfoldl_rev {M : monad} (T R : UU0) (f : R -> T -> R) (z : R) (s : seq T -> M (seq T)) : foldl f z (o) (rev (o) s) = foldr (fun x => f^~ x) z (o) s.
proof: Proof. apply boolp.funext => x; rewrite !fcompE 3!fmapE !bindA. bind_ext => ?; by rewrite bindretf /= -foldl_rev. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy