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