proposition: Lemma refin_writeList_rcons_cat_aswap (i : nat) x (ys zs : seq E) : writeList i (rcons (ys ++ zs) x) >> aswap (M := M) (i + size ys) (i + size (ys ++ zs)) `<=` qperm zs >>= (fun zs' => writeList i (ys ++ x :: zs')).
proof: Proof. under [in X in _ `<=` X]eq_bind do rewrite writeList_cat. rewrite (plus_commute (qperm zs))//. rewrite rcons_cat writeList_cat bindA. apply: refin_bindl => -[]; rewrite size_cat/= addnA. exact: refin_writeList_rcons_aswap. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib