proposition: Lemma refin_writeList_cons_aswap (i : nat) x (s : seq E) : writeList i (x :: s) >> aswap (M := M) i (i + size s) `<=` qperm s >>= (fun s' => writeList i (rcons s' x)).
proof: Proof. elim/last_ind: s => [|t h ih] /=. rewrite qperm_nil bindmskip bindretf addn0 aswapxx /= bindmskip. exact: refin_refl. rewrite bindA. apply: (refin_trans _ (refin_bindr _ (qperm_refin_cons _ _ _))). by rewrite bindretf -bindA -writeList_aswap; exact: refin_refl. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib