proposition: Lemma elements_spec : forall A dom (m : t A dom) xv, InA (X.eq * eq)%signature xv (elements m) <-> find (fst xv) m = Some (snd xv).
proof: Proof. intros A dom m [x v]. unfold elements. simpl. split; intro Hin. + apply S.find_1, S.elements_2. assumption. + apply S.find_2. assumption. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface