proposition: Lemma repr_D : forall i j, repr t i j -> exists n, D t i n.
proof: Proof. induction 1. exists O. apply DO. auto. destruct IHrepr. exists (S x). eapply DS; eauto. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)