proposition: Theorem funcCollision_true_cons : forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B) (ls : list (A * B)) a, funcCollision _ _ ls = true -> funcCollision _ _ (a :: ls) = true.
proof: Proof. unfold funcCollision. intuition. simpl in *. destruct (findCollision_1 eqda eqdb ls a0 b0). trivial. trivial. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv