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