proposition: Theorem list_pred_arrayLookupOpt : forall (A B C : Set)(P : B -> C -> Prop)(eqda : EqDec A)(ls1 : list (option (A * B)))(ls2 : list (option (A * C))), list_pred (fun o1 o2 => match o1 with | None => o2 = None | Some x => match o2 with | None => False | Some y => fst x = fst y /\ P (snd x) (snd y) end end) ls1 ls2 -> forall a, match (arrayLookupOpt _ ls1 a) with | None => (arrayLookupOpt _ ls2 a) = None | Some x => exists y, (arrayLookupOpt _ ls2 a) = Some y /\ P x y end.
proof: Proof. induction 1; intuition; simpl in *. trivial. destruct a1. destruct a2. destruct p. simpl in *. intuition. subst. destruct p0. simpl in *. case_eq (eqb a a0); intuition. econstructor. intuition. eapply IHlist_pred. destruct p. case_eq (eqb a a0); intuition. subst. eapply IHlist_pred. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold