proposition: Lemma equal_1 : forall m (Hm:Sort m) m' (Hm': Sort m') cmp, Equivb cmp m m' -> equal cmp m m' = true.
proof: Proof. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb; intuition; subst. match goal with H: compare _ _ = _ |- _ => clear H end. assert (cmp_e_e':cmp e e' = true). apply H1 with x; auto. rewrite cmp_e_e'; simpl. apply IHb; auto. inversion_clear Hm; auto. inversion_clear Hm'; auto. unfold Equivb; intuition. destruct (H0 k). assert (In k ((x,e) ::l)). destruct H as (e'', hyp); exists e''; auto. destruct (In_inv (H2 H4)); auto. inversion_clear Hm. elim (Sort_Inf_NotIn H6 H7). destruct H as (e'', hyp); exists e''; auto. apply MapsTo_eq with k; auto. destruct (H0 k). assert (In k ((x,e') ::l')). destruct H as (e'', hyp); exists e''; auto. destruct (In_inv (H3 H4)); auto. subst. inversion_clear Hm'. now elim (Sort_Inf_NotIn H5 H6). apply H1 with k; destruct (eq_dec x k); auto. destruct (compare x x') as [Hlt|Heq|Hlt]; try contradiction; clear y. destruct (H0 x). assert (In x ((x',e')::l')). apply H; auto. exists e; auto. destruct (In_inv H3). apply lt_not_eq in Hlt; now contradict Hlt. inversion_clear Hm'. assert (Inf (x,e) l'). apply Inf_lt with (x',e'); auto. elim (Sort_Inf_NotIn H5 H7 H4). destruct (H0 x'). assert (In x' ((x,e)::l)). apply H2; auto. exists e'; auto. destruct (In_inv H3). subst; apply lt_not_eq in Hlt; now contradict Hlt. inversion_clear Hm. assert (Inf (x',e') l). apply Inf_lt with (x,e); auto. elim (Sort_Inf_NotIn H5 H7 H4). destruct m; destruct m';try contradiction. clear H1;destruct p as (k,e). destruct (H0 k). destruct H1. exists e; auto. inversion H1. destruct p as (x,e). destruct (H0 x). destruct H. exists e; auto. inversion H. destruct p;destruct p0;contradiction. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses