proposition: Lemma writeList_cons i (x : E) (xs : seq E) : writeList i (x :: xs) = aput i x >> writeList i.+1 xs.
proof: Proof. by rewrite /writeList; unlock. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib