proposition: Lemma boundage : forall n, bounded t n -> bounded (t [a>- b]) n.
proof: Proof. unfold bounded. intros. destruct (H x). destruct (D_update_ex _ _ H0). exists x1. auto. lia. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)