proposition: Lemma compat_union_eq `{WF} {t'} `{WF t'} : t [=T=] t' -> forall x y, union t x y [=T=] union t' x y.
proof: Proof. intros H' x y. split; intros; apply le_incr; auto; apply H'. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)