proposition: Lemma write2LE i a b D (f : nat * nat -> M D) : write2L i (a, b) >>= f = writeList i (a ++ b) >> f (size a, size b).
proof: Proof. by rewrite /write2L bindA bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib