proposition: Lemma eq_leibniz : forall s s', eq s s' -> s = s'.
proof: Proof. intros [xs Hxs] [ys Hys] Heq. change (equivlistA X.eq xs ys) in Heq. assert (H : eqlistA X.eq xs ys). { rewrite <- Raw.isok_iff in Hxs, Hys. apply SortA_equivlistA_eqlistA with X.lt; auto with *. } apply eq_leibniz_list in H. subst ys. f_equal. apply Eqdep_dec.eq_proofs_unicity. intros x y; destruct (bool_dec x y); tauto. Qed.
imports: MSetInterface OrdersFacts OrdersLists