proposition: Lemma test_and_unify_eq : forall {uf} `{WF uf} x y, test_and_unify uf x y = (fst (equiv uf x y), union uf x y).
proof: Proof. intros uf Hwf x y; unfold test_and_unify, union, equiv; repeat (case find_spec; intros; auto). num_analyse; subst; reflexivity. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)