proposition: Lemma repr_x_inv_upd : forall x, repr t x a -> repr (t[ b>- a]) x a.
proof: Proof. induction 1. apply rzero. map_iff; intros [H' | H']; subst; tauto_false. destruct (eq_num_dec i b). subst. apply (rsucc _ b r). 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)