proposition: Lemma le_union `{WF}: forall x y, t <T= union t x y.
proof: Proof. intros x y. unfold le. intros a b ? . rewrite sameclass_union; trivial. intuition. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)