proposition: Lemma of_list_1b : forall 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 k Hnodup. - apply empty_o. - unfold uncurry; simpl. inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. specialize (IH k Hnodup'); clear Hnodup'. rewrite add_o, IH. unfold eqb; do 2 destruct eq_dec as [|?Hnot]; auto; elim Hnot; eauto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface