proposition: Theorem arrayLookup_In_split : forall (A B : Set)(eqda : EqDec A)(ls : list (A * B))(a : A)(b : B), arrayLookup _ ls a = Some b -> In a (fst (split ls)).
proof: Proof. induction ls; intuition; simpl in *. discriminate. case_eq (eqb a a0); intuition. rewrite H0 in H. inversion H; clear H; subst. rewrite eqb_leibniz in H0. subst. remember (split ls) as x. destruct x. simpl. intuition. rewrite H0 in H. remember (split ls) as x. destruct x. simpl. right. eapply IHls. eauto. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime