proposition: Lemma partition_ok1' : forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt), In x (fst (partition f s)) -> In x s.
proof: Proof. induction s; simpl; auto; intros. inv. generalize (IHs H1 f x). destruct (f a); destruct (partition f s); simpl in *; auto. inversion_clear H; auto. Qed.
imports: MSetInterface