proposition: Theorem compMap_randomFunc_NoDup : forall (A B C: Set){eqda : EqDec A}{eqdb : EqDec B}{eqdc : EqDec C}(ls : list A)(f : A -> B -> Comp C)(rndB : Comp B)(lsf : list (A * B)), NoDup ls -> (forall a, In a ls -> arrayLookup _ lsf a = None) -> comp_spec (fun a b => fst a = fst b) ((oc_compMap _ (fun x => y <--$ query x; $ f x y) ls) _ _ (@randomFunc A B rndB _) lsf) ((oc_compMap _ (fun x => y <--$ query x; $ f x y) ls) _ _ (fun s a => b <-$ rndB; ret (b, s)) tt).
proof: Proof. induction ls; intuition; simpl in *. comp_simp. eapply comp_spec_ret; intuition. inversion H; clear H; subst. simpl; inline_first. unfold randomFunc. rewrite H0. inline_first. comp_skip. comp_simp. inline_first. comp_skip. comp_simp. comp_skip. eapply IHls; intuition. simpl. case_eq (eqb a0 a); intuition. rewrite eqb_leibniz in H7. subst. intuition. comp_simp. simpl in *; subst. eapply comp_spec_ret; intuition. intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.PRF