proposition: Theorem randomFunc_withDups_spec : forall x1 x2 a, (forall x, arrayLookup _ x1 x = arrayLookup _ x2 x) -> comp_spec (fun y1 y2 : Bvector eta * list (D * Bvector eta) => fst y1 = fst y2 /\ (forall a0 : D, arrayLookup D_EqDec (snd y1) a0 = arrayLookup D_EqDec (snd y2) a0)) (randomFunc ({ 0 , 1 }^eta) D_EqDec x1 a) (randomFunc_withDups x2 a).
proof: Proof. intuition. unfold randomFunc, randomFunc_withDups. rewrite H. case_eq (arrayLookup D_EqDec x2 a); intuition. fcf_simp. fcf_spec_ret. simpl. case_eq (eqb a0 a); intuition. rewrite eqb_leibniz in H1. subst. rewrite H. trivial. fcf_skip. fcf_spec_ret. simpl. rewrite H. trivial. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF