proposition: Lemma link_main_lemma : forall x y, repr t x a -> repr t y b -> forall u v, (Equiv (t[ b>- a]) u v <-> (Equiv t u v \/ ((Equiv t u x /\ Equiv t v y) \/ (Equiv t v x /\ Equiv t u y)))).
proof: Proof. split; intros. unfold Equiv in H1. destruct H1 as [ruv Hu Hv]. destruct (eq_num_dec ruv a). subst. destruct (link_lemma_1 _ Hu); destruct (link_lemma_1 _ Hv); try solve [firstorder]. apply link_lemma_2 in Hu; auto. apply link_lemma_2 in Hv; auto. firstorder. destruct H1 as [[ruv Hu Hv] | [[[ru Hu Hx] [rv Hv Hy]] | [[ru Hu Hx] [rv Hv Hy]]]]. destruct (eq_num_dec ruv a). subst. exists a; eauto. destruct (eq_num_dec ruv b). subst. exists a; firstorder. exists ruv; firstorder. assert ( Hrua := repr_inj_right _ _ _ H _ Hx). assert ( Hrvb := repr_inj_right _ _ _ H0 _ Hy). rewrite <- Hrua, <- Hrvb in *. clear Hrua Hrvb. exists a. firstorder. firstorder. assert ( Hrua := repr_inj_right _ _ _ H _ Hx). assert ( Hrvb := repr_inj_right _ _ _ H0 _ Hy). rewrite <- Hrua, <- Hrvb in *. clear Hrua Hrvb. exists a. firstorder. firstorder. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)