proposition: Lemma equal_1 : forall m m' {Hm:Ok m}{Hm': Ok m'} cmp, Equivb cmp m m' -> equal cmp m m' = true.
proof: Proof. induction m as [|(k,e) m IH]; destruct m' as [|(k',e') m']; simpl. - trivial. - intros _ _ cmp (H,_). exfalso. specialize (H k'). rewrite In_nil, In_cons in H. rewrite H. now left. - intros _ _ cmp (H,_). exfalso. specialize (H k). rewrite In_nil, In_cons in H. rewrite <- H. now left. - intros Hm Hm' cmp E. inversion_clear Hm; inversion_clear Hm'. case X.compare_spec; intros E'. + apply andb_true_intro; split. * eapply E; eauto. apply InA_cons; now left. * apply IH; clear IH; trivial. destruct E as (E1,E2). split. { intros x. clear E2. split; intros; SortLt. specialize (E1 x); rewrite 2 In_cons in E1; simpl in E1. destruct E1 as ([E1|E1],_); eauto. MX.order. specialize (E1 x); rewrite 2 In_cons in E1; simpl in E1. destruct E1 as (_,[E1|E1]); eauto. MX.order. } { intros x xe xe' Hx HX'. eapply E2; eauto. } + assert (IN : In k ((k',e')::m')). { apply E. apply In_cons; now left. } apply In_cons in IN. simpl in IN. destruct IN as [?|IN]. MX.order. SortLt. MX.order. + assert (IN : In k' ((k,e)::m)). { apply E. apply In_cons; now left. } apply In_cons in IN. simpl in IN. destruct IN as [?|IN]. MX.order. SortLt. MX.order. Qed.
imports: Coq(OrdersFacts OrdersLists)