proposition: Lemma aput_writeListCR i j (x : E) (xs : seq E) : j + size xs <= i -> aput i x >> writeList j xs = writeList j xs >> aput i x.
proof: Proof. by move=> ?; rewrite -writeList1 -writeListC. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib