proposition: Lemma writeListRet i x (s : seq E) : writeList i (x :: s) >> Ret x = writeList i (x :: s) >> aget i.
proof: Proof. elim/last_ind: s x i => [|h t ih] /= x i. by rewrite bindmskip write_read. rewrite writeList_rcons 2![in RHS]bindA. rewrite write_readC; last by rewrite gtn_eqF// ltn_addr. rewrite -2![RHS]bindA -ih [RHS]bindA. rewrite !bindA; bind_ext => _. by under [in RHS]eq_bind do rewrite bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib