proposition: Lemma sameclass_find : forall `{WF} x, sameclass t (fst (find t x)) x.
proof: Proof. intros t Hwf x. case (find_spec); intros; auto. simpl. unfold sameclass. rewrite Heq; clear Heq. exists rx; [eapply repr_idem; eauto | eauto]. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)