proposition: Lemma class_of_union_2: forall `{WF} x y z, ~ sameclass t x z -> ~ sameclass t y z -> NumSet.Equal (class_of (union t x y) z) (class_of t z).
proof: Proof. intros t Hwf x y z Hxz Hyz u. setoid_rewrite <- sameclass_class_of. rewrite sameclass_union. intuition. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)