proposition: Lemma eq_equal : forall m m', eq m m' <-> equal m m' = true.
proof: Proof. intros (l,Hl); induction l. intros (l',Hl'); unfold eq; simpl. destruct l'; unfold equal; simpl; intuition. intros (l',Hl'); unfold eq. destruct l'. destruct a; unfold equal; simpl; intuition. destruct a as (x,e). destruct p as (x',e'). unfold equal; simpl. destruct (compare x x') as [Hlt|Heq|Hlt]; simpl; intuition. unfold cmp at 1. case (compare e e'); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH); clear HH; simpl. inversion_clear Hl. inversion_clear Hl'. destruct (IHl H (Build_slist H2)). unfold equal, eq in H5; simpl in H5; auto. destruct (andb_prop _ _ H); clear H. generalize H0; unfold cmp. case (compare e e'); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH); 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: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses