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