proposition: Theorem arrayLookup_In_split : forall (A B : Set)(eqd : EqDec A)(ls : list (A * B)) a b, arrayLookup _ ls a = Some b -> In a (fst (split ls)).
proof: Proof. induction ls; intuition idtac; simpl in *. discriminate. remember (split ls) as z. destruct z. simpl. case_eq (eqb a a0); intros. rewrite eqb_leibniz in H0. subst. intuition idtac. rewrite H0 in H. eauto. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold