proposition: Lemma writeListC i j (ys zs : seq E) : i + size ys <= j -> writeList i ys >> writeList j zs = writeList j zs >> writeList i ys.
proof: Proof. elim: ys zs i j => [|h t ih] zs i j hyp /=; first by rewrite bindretf bindmskip. rewrite aput_writeListC// bindA aput_writeListC; last first. by rewrite (leq_trans _ hyp)//= -addSnnS ltn_addr. rewrite -!bindA ih// addSn. by rewrite /= addnS in hyp. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib