proposition: Theorem arrayLookup_not_In_split : forall (A B : Set)(eqda : EqDec A)(ls : list (A * B))(a : A), arrayLookup _ ls a = None -> ~In a (fst (split ls)).
proof: Proof. induction ls; intuition; simpl in *. case_eq (eqb a a0); intuition; rewrite H1 in H. discriminate. remember (split ls) as x. destruct x. simpl in *. intuition; subst. rewrite eqb_refl in H1. discriminate. eauto. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime