proposition: Lemma writeList_cat i (s1 s2 : seq E) : writeList i (s1 ++ s2) = writeList i s1 >> writeList (i + size s1) s2.
proof: Proof. elim: s1 i => [|h t ih] i/=; first by rewrite addn0 bindretf. by rewrite ih bindA addSnnS. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib