proposition: Theorem sortedRandomFunc_sorted_equiv : forall s a, comp_spec (fun s1 s2 => fst s1 = fst s2 /\ (snd s2) = sortDom (snd s1)) (@randomFunc A B rndB _ s a) (sortedRandomFunc (sortDom s) a).
proof: Proof. intuition idtac. unfold randomFunc, sortedRandomFunc. rewrite <- arrayLookup_sortDom_eq. case_eq (arrayLookup A_EqDec s a); intuition idtac. eapply comp_spec_ret; intuition idtac. fcf_skip. eapply comp_base_exists; eauto. eapply comp_base_exists; eauto. eapply comp_spec_ret; intuition idtac. Qed.
imports: FCF FCF.PRF Permutation