proposition: Lemma of_list_1 l k e : NoDupA eqk l -> (MapsTo k e (of_list l) <-> InA eqke (k,e) l).
proof: Proof. revert k e. induction l as [|(k',e') l IH]; simpl; intros k e Hnodup. - rewrite empty_mapsto_iff, InA_nil; intuition. - unfold uncurry; simpl. inversion_clear Hnodup as [| ? ? Hnotin Hnodup']. specialize (IH k e Hnodup'); clear Hnodup'. rewrite add_mapsto_iff, InA_cons, <- IH. unfold eq_key_elt, Duo at 1; simpl. split; destruct 1 as [H|H]; try (intuition (auto with map);fail). destruct (K.eq_dec k k'); [left|right]; split; auto with map. contradict Hnotin. apply InA_eqke_eqk with k e; intuition. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)