proposition: Theorem funcCollision_false_impl_collidesWith_false : forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B) ls (a : A) (b : B), funcCollision _ _ ls = false -> In (a, b) ls -> collidesWith _ _ ls a b = false.
proof: Proof. induction ls; intuition; simpl in *. intuition. pairInv. unfold collidesWith, funcCollision in *. simpl in *. repeat rewrite eqb_refl. simpl. case_eq (findCollision_1 eqda eqdb ls a b1); intuition. rewrite H0 in H. discriminate. unfold collidesWith, funcCollision in *. simpl in *. case_eq (eqb a0 a); intuition. rewrite eqb_leibniz in H0. subst. rewrite eqb_refl. simpl. case_eq (findCollision_1 eqda eqdb ls a b0); intuition; rewrite H0 in H. discriminate. case_eq (eqb b1 b0); intuition. simpl. eapply IHls; intuition. simpl. eapply IHls; intuition. assert (a <> a0). intuition. subst. rewrite eqb_refl in H0. discriminate. case_eq (eqb a a0); intuition. rewrite eqb_leibniz in H3. subst. intuition. simpl. case_eq (eqb b1 b0); intuition. simpl. rewrite eqb_leibniz in H4. subst. specialize (in_impl_collidesWith _ _ ls _ H1 H2); intuition. unfold collidesWith in H4. destruct (findCollision_1 eqda eqdb ls a0 b0); discriminate. simpl. case_eq (findCollision_1 eqda eqdb ls a0 b0); intuition. rewrite H5 in H. discriminate. rewrite H5 in H. eapply IHls; intuition. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv