proposition: Lemma writeList_rcons i (x : E) (xs : seq E) : writeList i (rcons xs x) = writeList i xs >> aput (i + size xs) x.
proof: Proof. by rewrite -cats1 writeList_cat /= -bindA bindmskip. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib