proposition: Lemma class_of_injective: forall `{WF} x y, NumSet.Equal (class_of t x) (class_of t y) -> {{t}} x y.
proof: Proof. intros. assert (NumSet.In y (class_of t y)). rewrite <- sameclass_class_of. reflexivity. rewrite <- H0 in H1. rewrite <- sameclass_class_of in H1. symmetry. auto. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)