proposition: Theorem arrayLookup_None_not_In : forall (A B : Set)(eqda : EqDec A)(ls : list (A * B)) a, arrayLookup _ ls a = None -> In a (fst (split ls)) -> False.
proof: Proof. induction ls; intuition; simpl in *. remember (split ls) as z. destruct z. simpl in *. intuition; subst. rewrite eqb_refl in H. discriminate. destruct (eqb a a0). discriminate. eauto. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold