proposition: Lemma aput_writeListC i j (x : E) (xs : seq E) : i < j -> aput i x >> writeList j xs = writeList j xs >> aput i x.
proof: Proof. elim: xs i j => [|h tl ih] i j ij /=; first by rewrite bindmskip bindretf. rewrite -bindA aputC; last by left; rewrite lt_eqF. by rewrite !bindA; bind_ext => -[]; rewrite ih// ltnW. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib