proposition: Lemma from_elements_spec : forall A (l : list (key * A)), NoDupA (X.eq@@1)%signature l -> forall x v, find x (from_elements l) = Some v <-> InA (X.eq * eq)%signature (x, v) l.
proof: Proof. intros A l Hnodup x v. unfold elements, from_elements, find. simpl. rewrite pre_from_elements_spec; trivial. + intuition. eelim S.empty_1. apply S.find_2; eassumption. + intros [?] _ [? Hin]; simpl in *. apply (S.empty_1 Hin). Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface