proposition: Theorem arrayLookup_flatten_eq : forall (A B C : Set)(eqda : EqDec A)(eqdb : EqDec B)(ls : list (list (A * B * C))) keys a b, list_pred (fun a b => forall x, In x b -> fst (fst x) = a) keys ls -> NoDup keys -> arrayLookup _ (flatten ls) (a, b) = arrayLookup _ (arrayLookupList _ (combine keys ls) a) (a, b).
proof: Proof. induction ls; intuition; simpl in *. inversion H; clear H; subst. simpl. trivial. inversion H; clear H; subst. simpl. unfold arrayLookupList. simpl. inversion H0; clear H0; subst. case_eq (eqb a0 a1); intuition. case_eq (arrayLookup (pair_EqDec eqda eqdb) a (a0, b)); intuition. eapply arrayLookup_app_Some. trivial. rewrite eqb_leibniz in H. subst. rewrite arrayLookup_app_None; intuition. eapply arrayLookup_pair_flatten_none. eauto. intuition. case_eq ( arrayLookup _ a (a0, b) ); intuition. rewrite arrayLookup_pair_None in H0. discriminate. intuition. subst. eapply eqb_false_iff in H. intuition. rewrite arrayLookup_app_None. eapply IHls; intuition. trivial. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold