proposition: Lemma of_list_1b l k : NoDupA eqk l -> find k (of_list l) = findA (eqb k) l.
proof: Proof. induction l as [|(k',e') l IH]; simpl; intros Hnodup. apply empty_o. unfold uncurry; simpl. inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. specialize (IH Hnodup'); clear Hnodup'. rewrite add_o, IH, eqb_sym. unfold eqb; now destruct K.eq_dec. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)