proposition: Lemma class_of_union: forall `{WF} x y, NumSet.Equal (class_of (union t x y) x) (NumSet.union (class_of t x) (class_of t y)).
proof: Proof. intros t Hwf x y z. rewrite <- sameclass_class_of. rewrite sameclass_union. NumSetProps.set_iff. setoid_rewrite <- sameclass_class_of. intuition. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)