proposition: Lemma subset_spec : forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'}, subset s s' = true <-> Subset s s'.
proof: Proof. unfold subset, Subset; intros. rewrite is_empty_spec. unfold Empty; intros. intuition. - specialize (H a). rewrite diff_spec in H; intuition. rewrite <- (mem_spec a) in H |- *. destruct (mem a s'); intuition auto with bool. - rewrite diff_spec in H0; intuition. Qed.
imports: MSetInterface