proposition: Lemma refin_dispatch_Ret_write3L_ipartl x ys zs : dispatch_Ret x p (ys, zs, xs) >>= write3L i >>= uncurry3 (ipartl (M := M) p i) `<=` dispatch_Ret x p (ys, zs, xs) >>= uncurry3 (qperm_partl p) >>= write2L i.
proof: Proof. by rewrite /= !if_bind; apply: refin_if => _; rewrite !bindA; apply/refin_bindl => zs'; rewrite !bindretf; exact: refin_write3L_ipartl. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)