proposition: Lemma class_of_In_repr' : forall `{WF} x z, repr (p t) x z -> NumSet.In z (class_of t x).
proof: Proof. intros t Hwf x z H. unfold class_of in *. induction H. NumSetProps.setdec. assert (H'' := class_of_In_MapsTo' _ _ H). revert IHrepr. NumSetProps.set_iff. intros [H' | H']; num_prop; subst. clear H0. revert H''. unfold class_of. NumSetProps.set_iff. intros [? | ?]; num_prop; auto. revert H''. unfold class_of. NumSetProps.set_iff. intros [? | ?]; num_prop. subst. auto. right. apply class_of_Equal_MapsTo in H. rewrite <- H. auto. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)