proposition: Lemma class_of_compat' : forall `{WF} {t'} `{WF t'} x, eq t t' -> NumSet.Equal (class_of t x) (class_of t' x).
proof: Proof. intros t Ht t' Ht' x H y. setoid_rewrite <- sameclass_class_of. rewrite H. reflexivity. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)