proposition: Lemma eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.
proof: Proof. intros (m,Hm); induction m; intros (m', Hm'); destruct m'; unfold eq; simpl; try destruct a as (x,e); try destruct p as (x',e'); auto. destruct (X.compare x x') as [Hlt|Heq|Hlt]; MapS.Raw.MX.elim_comp; intuition auto with ordered_type. inversion_clear Hm; inversion_clear Hm'. apply (IHm H0 (Build_slist H4)); auto. Qed.
imports: FMapInterface