proposition: Lemma repr_helper `{WF} x: exists z, repr (p t) x z.
proof: Proof. destruct (@wf _ H x). clear H1. induction H0. exists i. apply rzero. auto. destruct IHD. exists x. eapply rsucc; eauto. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)