proposition: Theorem arrayLookupList_pred' : forall (A B : Set) (eqda : EqDec A) (P : list B -> Type) (ls : list (A * list B)) (a : A), (forall x : list B, In (a, x) ls -> P x) -> (arrayLookup _ ls a = None -> P nil) -> P (arrayLookupList eqda ls a).
proof: Proof. induction ls; intuition; simpl in *. unfold arrayLookupList. simpl. case_eq (eqb a a0); intuition. eapply X. rewrite eqb_leibniz in H. subst. intuition. case_eq (arrayLookup eqda ls a); intuition. specialize (IHls a). unfold arrayLookupList in *. rewrite H0 in IHls. eapply IHls; eauto. intuition. discriminate. rewrite H in X0. intuition. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold