proposition: Lemma equal_spec: forall s s', equal s s' = true <-> Equal s s'.
proof: Proof. intros. rewrite equal_subset. rewrite andb_true_iff. rewrite 2subset_spec. unfold Equal, Subset. firstorder. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface