proposition: Lemma repr_update_fwd : forall y, repr t y b -> repr (t[ b>- a]) y a.
proof: Proof. induction 1. apply (rsucc _ i a). map_iff; auto. apply rzero. map_iff. intros [H' | H']. subst. tauto_false. revert H'. eapply repr_inv_In. eauto. destruct (eq_num_dec i r). subst. apply (rsucc _ r a). map_iff; auto. apply rzero. eauto. eapply rsucc. 2: apply IHrepr; auto. map_iff. auto. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)