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