proposition: Lemma write3LE i x D (f : nat * nat * nat -> M D) : write3L i x >>= f = let '(s, t, u) := x in writeList i (s ++ t ++ u) >> f (size s, size t, size u).
proof: Proof. by move: x => -[[x y] z]; rewrite /write3L bindA bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib