proposition: Theorem arrayLookup_pair_None : forall (A B C : Set)(eqda : EqDec A)(eqdb : EqDec B) (ls : list (A * B * C)) a b, (forall x, In x ls -> fst (fst x) <> a) -> arrayLookup _ ls (a, b) = None.
proof: Proof. induction ls; intuition; simpl in *. case_eq (eqbPair eqda eqdb (a0, b1) (a, b0)); intuition. exfalso. unfold eqbPair in *. simpl in *. apply andb_true_iff in H0. intuition. rewrite eqb_leibniz in H1. subst. eapply H. left. reflexivity. trivial. eauto. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold