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