proposition: Lemma eq_union `{WF}: forall x y, {{t}} x y -> t [=T=] union t x y.
proof: Proof. intros x y Hxy. split. apply le_union; trivial. intros a b H'. rewrite sameclass_union in H'; trivial. intuition. rewrite H0, Hxy, H2. reflexivity. rewrite H0, Hxy, H2. reflexivity. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)