proposition: Theorem arrayLookupList_pred : forall (A B : Set) (eqda : EqDec A)P (ls : list (A * list B)) a, (forall x, In x ls -> P (snd x)) -> P nil -> P (arrayLookupList _ ls a).
proof: Proof. induction ls; intuition; simpl in *. unfold arrayLookupList. simpl. case_eq (eqb a a0); intuition. specialize (X (a0, b)). intuition. eapply IHls; intuition. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold