proposition: Theorem in_impl_collidesWith : forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B)(ls : list (A * B))(a a': A) (b : B), In (a, b) ls -> a <> a' -> collidesWith _ _ ls a' b = true.
proof: Proof. unfold collidesWith in *. induction ls; intuition; simpl in *. intuition. pairInv. case_eq (eqb a' a); intuition. rewrite eqb_leibniz in H. subst. intuition. rewrite eqb_refl. simpl in *. trivial. case_eq (eqb b1 b0); intuition. case_eq (eqb a' a0); intuition. simpl. eapply IHls; intuition. eauto. subst; intuition. simpl. eapply IHls; eauto. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv