fact: Axiom sameclass_union : forall `{WF} a b x y, sameclass (union t a b) x y <-> (sameclass t x y \/ (sameclass t x a /\ sameclass t y b) \/ (sameclass t y a /\ sameclass t x b)).
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)