proposition: Lemma eq_leibniz_list : forall xs ys, eqlistA X.eq xs ys -> xs = ys.
proof: Proof. induction xs as [|x xs]; intros [|y ys] H; inversion H; [ | ]. - reflexivity. - f_equal. + apply X.eq_leibniz; congruence. + apply IHxs; subst; assumption. Qed.
imports: MSetInterface OrdersFacts OrdersLists