proposition: Lemma slowsort_preserves_size2 (x : seq E) B (f : seq E -> nat -> M B) : (slowsort x >>= fun x' => f x' (size x)) = (slowsort x >>= fun x' => f x' (size x')) :> M _.
proof: Proof. transitivity (slowsort x >>= (fun y => Ret (y, size y)) >>= (fun z => f z.1 z.2)). by rewrite slowsort_preserves_size bindA; bind_ext => s; rewrite bindretf. by rewrite bindA; bind_ext => s; rewrite bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib infotheo(ssr_ext) Recdef Equations(Equations) mathcomp(ssrnat)