proposition: Lemma equal_2 m m' {Hm:Ok m}{Hm':Ok m'} cmp : equal cmp m m' = true -> Equivb cmp m m'.
proof: Proof. revert m' Hm'. induction m as [|(k,e) m IH]; destruct m' as [|(k',e') m']; simpl; try discriminate. - split. red. reflexivity. inversion 1. - intros Hm'. case X.compare_spec; try discriminate. rewrite andb_true_iff. intros E (C,EQ). inversion_clear Hm; inversion_clear Hm'. apply IH in EQ; trivial. destruct EQ as (E1,E2). split. + intros x. rewrite 2 In_cons; simpl. rewrite <- (E1 x). intuition; now left; MX.order. + intros x ex ex'. unfold MapsTo in *. rewrite 2 InA_cons, 2 eqke_def. intuition; subst. * trivial. * SortLt. MX.order. * SortLt. MX.order. * eapply E2; eauto. Qed.
imports: Coq(OrdersFacts OrdersLists)