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