proposition: Lemma le_incr `{WF} {t'} `{WF t'}: forall x y, t <T= t' -> union t x y <T= union t' x y.
proof: Proof. intros x y ? u v. rewrite 2 sameclass_union. intuition. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)