proposition: Lemma of_list_1 : forall l k e, NoDupA eqk l -> (MapsTo k e (of_list l) <-> InA eqke (k,e) l).
proof: Proof. 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 at 1; simpl. split; destruct 1 as [H|H]; try (intuition;fail). destruct (eq_dec k k'); [left|right]; split; auto. contradict Hnotin. apply InA_eqke_eqk with k e; intuition. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface