proposition: Lemma MapsTo_sameclass : forall `{WF} x z, NumMap.MapsTo x z (p t) -> sameclass t x z.
proof: Proof. intros. destruct (repr_helper x) as [y ?]; auto. exists y. auto. inversion H1; subst. firstorder. assert (j = z). NumMapProps.find_tac. subst. auto. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)