proposition: Lemma assert_all_scanl s (xs : seq A) : assert (all ok \o scanl op s) xs = protect (scanlM op s xs >>= (fun ys => guard (all ok ys) >> Ret xs)) :> M _.
proof: Proof. rewrite assertE guardsC; last exact: bindmfail. transitivity (protect (scanlM op s xs) >>= (fun ys => guard (all ok ys) >> Ret xs) : M _). by rewrite -!bindA -scanlM_of_scanl bindA !bindretf assertE. rewrite bindA [in RHS]/protect. bind_ext => st. rewrite 2!bindA; bind_ext => xs'. rewrite [in RHS]bindA [in RHS]guardsC; last exact: bindmfail. rewrite bindA bindretf. rewrite /overwrite bindA bindretf bindA; bind_ext; case. by rewrite bindretf assertE. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib