proposition: Theorem randomFunc_mem_preserves_coll : forall (D1 D2 R : Set)(eqdd : EqDec D1)(eqdd2 : EqDec D2)(eqdr : EqDec R) (RndR : Comp R) (c0 : list ((D1 * D2) * R)) d a b0, funcCollision _ _ (fst (split c0)) = true -> In (a, b0) (getSupport (randomFunc_mem _ _ RndR c0 d)) -> funcCollision _ _ (fst (split b0)) = true.
proof: Proof. intuition. unfold randomFunc_mem in *. destruct (arrayLookup _ c0 (a, b0)). repeat simp_in_support. simpl in *. remember (split c0) as z. destruct z. simpl in *. eapply funcCollision_true_cons; eauto. repeat simp_in_support. simpl in *. remember (split c0) as z. destruct z. simpl in *. eapply funcCollision_true_cons; eauto. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv