proposition: Theorem arrayLookup_In_NoDup : forall (A B : Set)(eqda : EqDec A)(ls : list (A * B)) a b, In (a, b) ls -> NoDup (fst (split ls)) -> arrayLookup _ ls a = Some b.
proof: Proof. induction ls; intuition; simpl in *. intuition. remember (split ls) as z. destruct z. intuition. pairInv. simpl in *. inversion H0; clear H0; subst. rewrite eqb_refl. trivial. simpl in *. inversion H0; clear H0; subst. case_eq (eqb a a0); intuition. rewrite eqb_leibniz in H. subst. eapply in_split_l in H1. rewrite <- Heqz in H1. simpl in *. intuition. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold