proposition: Lemma writeList_ret_aget i x (s : seq E) (f : E -> M (nat * nat)%type): writeList i (x :: s) >> Ret x >> f x = writeList i (x :: s) >> aget i >>= f.
proof: Proof. rewrite writeListRet 2!bindA /=. rewrite aput_writeListC//. rewrite 2!bindA. under [LHS] eq_bind do rewrite -bindA aputget. by under [RHS] eq_bind do rewrite -bindA aputget. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib