proposition: Lemma link_lemma_1 : forall z, repr (t[ b>- a]) z a -> (repr t z a \/ repr t z b).
proof: Proof. induction 1. left. apply rzero. intro; apply H. map_iff; auto. destruct (eq_num_dec i b). subst. right; apply rzero. eapply repr_inv_In. eauto. revert H. map_iff. intros [[H' H''] | [H' H'']]. subst. tauto_false. destruct IHrepr. left; eapply rsucc; eauto. right; eapply rsucc; eauto. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)