proposition: Theorem list_pred_impl_arrayLookup : forall (A B C : Set) P (eqda : EqDec A)(ls1 : list (A * B))(ls2 : list (A * C)), list_pred (fun x y => fst x = fst y /\ P (snd x) (snd y)) ls1 ls2 -> (forall v z, arrayLookup _ ls1 v = Some z -> exists z', arrayLookup _ ls2 v = Some z' /\ P z z') /\ (forall v, arrayLookup _ ls1 v = None -> arrayLookup _ ls2 v = None).
proof: Proof. induction 1; intros; simpl in *. intuition. discriminate. destruct a1. destruct a2. destruct H. simpl in *. subst. intuition. case_eq (eqb v a0); intuition. rewrite H4 in H3. inversion H3; clear H3; subst. econstructor; eauto. rewrite H4 in H3. edestruct H. eauto. intuition. case_eq (eqb v a0); intuition. rewrite H4 in H3. discriminate. rewrite H4 in H3. eauto. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold