proposition: Lemma find_spec : forall `{WF} x, find_spec_decl t x (find t x).
proof: Proof. intros t Hwf x. case_eq (find t x) ; intros rx t' H. unfold find in H. case_eq (find_aux (size t) x (p t)). intros rx' t'' H'; rewrite H' in *. injection H. intros; subst. clear H. constructor; destruct (@wf _ Hwf x) as [n Hxn Hn]; destruct (find_equiv _ (size t) _ _ _ _ _ H' Hxn Hn) as [Hrx [[?|?] [Heq Hb]]]; subst; simpl; auto; try apply Hwf. rewrite <- D_repr. auto. eapply rsucc. eauto. rewrite <- D_repr. auto. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)