proposition: Lemma D_inj : forall x n , D t x n -> forall m, D t x m -> n = m.
proof: Proof. induction 1; inversion_clear 1; find_tac. apply IHD in H3. congruence. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)