proposition: Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp, equal cmp m m' = true -> Equivb cmp m m'.
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; try discriminate; subst; try match goal with H: compare _ _ = _ |- _ => clear H end. inversion H0. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. destruct (IHb H1 H3 H6). destruct (In_inv H0). exists e'; constructor; split; trivial; apply eq_trans with x; auto. destruct (H k). destruct (H9 H8) as (e'',hyp). exists e''; auto. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. destruct (IHb H1 H3 H6). destruct (In_inv H0). exists e; constructor; split; trivial; apply eq_trans with x'; auto. destruct (H k). destruct (H10 H8) as (e'',hyp). exists e''; auto. inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. destruct (IHb H2 H4 H7). inversion_clear H0. destruct H9; simpl in *; subst. inversion_clear H1. destruct H0; simpl in *; subst; auto. elim (Sort_Inf_NotIn H4 H5). exists e'0; apply MapsTo_eq with x; auto. inversion_clear H1. destruct H0; simpl in *; subst; auto. elim (Sort_Inf_NotIn H2 H3). exists e0; apply MapsTo_eq with x; auto. apply H8 with k; auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses