proposition: Theorem arrayLookup_noCollision_eq : forall (A B C : Set)(eqda : EqDec A)(eqdb : EqDec B)(x1 : list ((A * B) * C)) a b0 b, arrayLookup _ x1 (a, b) = Some b0 -> collidesWith _ _ (fst (split x1)) a b = false -> arrayLookup_f _ x1 b = Some b0.
proof: Proof. induction x1; intuition; simpl in *. remember (split x1) as z. destruct z. simpl in *. unfold collidesWith in *. simpl in *. case_eq (eqb b3 b1); intuition. rewrite H1 in H0. simpl in *. case_eq (eqb a0 a); intuition. rewrite H2 in H0. simpl in *. rewrite eqb_leibniz in H1. rewrite eqb_leibniz in H2. subst. unfold eqbPair in *. simpl in *. repeat rewrite eqb_refl in H. simpl in *. trivial. rewrite H2 in H0. simpl in *. discriminate. rewrite H1 in H0. simpl in *. unfold eqbPair in *. simpl in *. rewrite H1 in H. case_eq (eqb a0 a); intuition. rewrite H2 in H. simpl in *. eapply IHx1; eauto. rewrite H2 in H. simpl in *. eapply IHx1; eauto. Qed.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv