proposition: Lemma class_of_empty: forall x, NumSet.Equal (class_of empty x) (NumSet.singleton x).
proof: Proof. intros x y. rewrite <- sameclass_class_of. split; intros H. rewrite (sameclass_empty _ _ H). apply NumSet.singleton_2. apply NumSet.E.eq_refl. replace y with x. reflexivity. apply -> set_eq_spec. apply NumSet.singleton_1, H. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)