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