proposition: Lemma repr_inv_upd : forall z rz, repr t z rz -> rz<>b -> repr (t[ b>- a]) z rz.
proof: Proof. induction 1; intros. apply rzero. map_iff. intros [H' | H']; subst; tauto_false. destruct (eq_num_dec i b); subst. apply repr_inv_In in repr_b. firstorder. eapply rsucc. 2 : eapply IHrepr; auto. map_iff. auto. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)