proposition: Theorem findCollision_correct : forall (A B : Set) eqd1 eqd2 (ls : list (A * B)) (x1 x2 : A) y, findCollision eqd1 eqd2 ls = Some (x1, x2, y) -> x1 <> x2 /\ In (x1, y) ls /\ In (x2, y) ls.
proof: Proof. induction ls; intros; simpl in *; subst; try discriminate. destruct a. case_eq (findCollision_1 eqd1 eqd2 ls a b0); intros. rewrite H0 in H. eapply findCollision_1_correct in H0. intuition. subst. inversion H; clear H; subst. intuition. inversion H; clear H; subst. intuition. inversion H; clear H; subst. intuition. rewrite H0 in H. eapply IHls in H. intuition. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv