proposition: Theorem F_randomFunc_preserves_coll : forall c0 x d a b0, funcCollision _ _ (fst (split c0)) = true -> In (a, b0) (getSupport (F_randomFunc x c0 d)) -> funcCollision _ _ (fst (split b0)) = true.
proof: Proof. intuition. unfold F_randomFunc in *. case_eq (arrayLookup_f (Bvector_EqDec b) c0 (F x d)); intuition. rewrite H2 in H1. repeat simp_in_support. simpl in *. remember (split c0) as z. destruct z. simpl in *. eapply funcCollision_true_cons; eauto. rewrite H2 in H1. 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