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; revert m' Hm'. induction Hm as [|[a e] m Hm IHHm Hr]; simpl in *; intros [|[a' e'] m'] Hm' H. + reflexivity. + destruct H as [H _]; specialize (H a') as [_ H]. destruct H; [exists e'; constructor; reflexivity|inversion H]. + destruct H as [H _]; specialize (H a) as [H _]. destruct H; [exists e; constructor; reflexivity|inversion H]. + apply Sorted_inv in Hm'; destruct Hm' as [Hm' Hr']. destruct (X.compare a a') as [Hlt|Heq|Hgt]; [exfalso| |exfalso]. - destruct H as [H _]; specialize (H a) as [H _]. destruct H as [e'' H]; [eexists; constructor; reflexivity|]. apply InA_cons in H; destruct H as [H|H]. * apply (gt_not_eq Hlt); symmetry; apply H. * apply InA_eqke_eqk, (Sort_Inf_In Hm' Hr') in H. compute in H; order. - apply andb_true_iff; split. * destruct H as [_ H]; apply H with a. { apply InA_cons_hd; reflexivity. } { apply InA_cons_hd; auto with ordered_type. } * apply IHHm; [assumption|]; split. { intros k; destruct H as [H _]; specialize (H k). split; intros [e'' Hk]. + destruct H as [H _]; destruct H as [e''' H]. - exists e''; apply InA_cons_tl; apply Hk. - apply InA_cons in H; destruct H as [[H _]|H]. * assert (Hs := Sort_Inf_In Hm Hr (InA_eqke_eqk Hk)). elim (gt_not_eq Hs); simpl; etransitivity; [eassumption|symmetry; assumption]. * exists e'''; assumption. + destruct H as [_ H]; destruct H as [e''' H]. - exists e''; apply InA_cons_tl; apply Hk. - apply InA_cons in H; destruct H as [[H _]|H]. * assert (Hs := Sort_Inf_In Hm' Hr' (InA_eqke_eqk Hk)). elim (gt_not_eq Hs); simpl; etransitivity; eassumption. * exists e'''; assumption. } { intros; destruct H as [_ H]; apply H with k; apply InA_cons_tl; assumption. } - destruct H as [H _]; specialize (H a') as [_ H]. destruct H as [e'' H]; [eexists; constructor; reflexivity|]. apply InA_cons in H; destruct H as [H|H]. * apply (gt_not_eq Hgt); symmetry; apply H. * apply InA_eqke_eqk, (Sort_Inf_In Hm Hr) in H. compute in H; order. Qed.
imports: FMapInterface