proposition: Lemma equal_spec : forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'}, equal s s' = true <-> Equal s s'.
proof: Proof. unfold Equal, equal; intros. rewrite andb_true_iff, !subset_spec. unfold Subset; intuition. - rewrite <- H; auto. - rewrite H; auto. Qed.
imports: MSetInterface