proposition: Lemma sameclass_union : forall {uf} `{WF uf} a b, forall s t, sameclass (union uf a b) s t <-> (sameclass uf s t \/ (sameclass uf s a /\ sameclass uf t b) \/ (sameclass uf t a /\ sameclass uf s b)).
proof: Proof. intros uf a b Hwf. unfold union. unfold sameclass. repeat (case find_spec; intros; auto). rewrite Heq, Heq0 in *. num_analyse. subst. intuition auto. exists rx0. destruct H0. rewrite (repr_inj_right _ _ _ Hrepr _ H0). auto. destruct H1. rewrite (repr_inj_right _ _ _ Hrepr0 _ H1). auto. exists rx0. destruct H1. rewrite (repr_inj_right _ _ _ Hrepr0 _ H1). auto. destruct H0. rewrite <- (repr_inj_right _ _ _ H0 _ Hrepr). auto. unfold link. unfold sameclass. case compare_spec; simpl; intro; rewrite link_main_lemma; eauto; intuition. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)