proposition: Lemma iqsort'_Fix (ni : nat * nat) (f g : forall (n'j : nat * nat), (n'j.2 < ni.2)%coq_nat -> M unit) : (forall (n'j : nat * nat) (p : (n'j.2 < ni.2)%coq_nat), f n'j p = g n'j p) -> iqsort' f = iqsort' g.
proof: Proof. by move=> ?; congr iqsort'; apply funext_dep => ?; apply boolp.funext. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)