proposition: Theorem arrayLookup_pair_flatten_none : forall (A B C : Set)(eqda : EqDec A)(eqdb : EqDec B) keys (ls : list (list (A * B * C))) a b, list_pred (fun a b => forall x, In x b -> fst (fst x) = a) keys ls -> (~ In a keys) -> arrayLookup (pair_EqDec eqda eqdb) (flatten ls) (a, b) = None.
proof: Proof. induction keys; intuition; simpl in *. inversion H; clear H; subst. simpl. trivial. inversion H; clear H; subst. intuition. simpl. case_eq (arrayLookup (pair_EqDec eqda eqdb) a2 (a0, b)); intuition. rewrite arrayLookup_pair_None in H0. discriminate. intuition. subst. eapply H. symmetry. eapply H3. trivial. rewrite arrayLookup_app_None; trivial. eauto. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold