proposition: Lemma class_of_Equal_repr : forall `{WF} x z, repr (p t) x z -> NumSet.Equal (class_of' t z) (class_of' t x).
proof: Proof. intros t Hwf x z H. induction H. reflexivity. apply class_of_Equal_MapsTo in H. rewrite IHrepr. assumption. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)