proposition: Lemma eq_equal : forall m m', eq m m' <-> equal cmp m m' = true.
proof: Proof. intros (l,Hl); induction l. - intros (l',Hl'); unfold eq; simpl. destruct l'; unfold equal; simpl; intuition auto with bool. - intros (l',Hl'); unfold eq. destruct l'. + destruct a; unfold equal; simpl; intuition auto with bool. + destruct a as (x,e). destruct p as (x',e'). unfold equal; simpl. destruct (X.compare x x') as [Hlt|Heq|Hlt]; simpl; intuition auto with bool. * unfold cmp at 1. MD.elim_comp; clear H; simpl. inversion_clear Hl. inversion_clear Hl'. destruct (IHl H (Build_slist H3)). unfold equal, eq in H5; simpl in H5; auto. * destruct (andb_prop _ _ H); clear H. generalize H0; unfold cmp. MD.elim_comp; auto; intro; discriminate. * destruct (andb_prop _ _ H); clear H. inversion_clear Hl. inversion_clear Hl'. destruct (IHl H (Build_slist H3)). unfold equal, eq in H6; simpl in H6; auto. Qed.
imports: FMapInterface