proposition: Lemma equal_spec : forall (s s' : t) (Hs : Ok s) (Hs' : Ok s'), equal s s' = true <-> Equal s s'.
proof: Proof. induction s as [ | x s IH]; intros [ | x' s'] Hs Hs'; simpl. - intuition reflexivity. - split; intros H. + discriminate. + assert (In x' nil) by (rewrite H; auto). inv. - split; intros H. + discriminate. + assert (In x nil) by (rewrite <-H; auto). inv. - inv. elim_compare x x' as C; try discriminate. + rewrite IH; auto. split; intros E y; specialize (E y). * rewrite !InA_cons, E, C; intuition. * rewrite !InA_cons, C in E. intuition; try sort_inf_in; order. + split; intros E. * discriminate. * assert (In x (x'::s')) by (rewrite <- E; auto). inv; try sort_inf_in; order. + split; intros E. * discriminate. * assert (In x' (x::s)) by (rewrite E; auto). inv; try sort_inf_in; order. Qed.
imports: MSetInterface OrdersFacts OrdersLists