proposition: Theorem arrayLookup_Some_impl_In : forall (A B : Set)(eqd : EqDec A)(ls : list (A * B)) a b, arrayLookup _ ls a = Some b -> In (a, b) 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. intuition. right. eauto. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold