proposition: Lemma elements_Sorted : forall A dom (m : t A dom), Sorted (X.lt@@1)%signature (elements m).
proof: Proof. intros A dom [m Hok]. unfold elements. simpl. apply S.elements_3. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface