proposition: Lemma class_of_Equal_MapsTo : forall `{WF} x z, NumMap.MapsTo x z (p t) -> NumSet.Equal (class_of' t z) (class_of' t x) .
proof: Proof. unfold class_of'. intros t Hwf x z H. intros y. apply MapsTo_sameclass in H; auto. rewrite (NumMap_fold_compat _ _ (fun a b acc => if fst (equiv t x a) && fst (equiv t x b) then NumSet.add a (NumSet.add b acc) else acc) (fun a b acc => if fst (equiv t z a) && fst (equiv t z b) then NumSet.add a (NumSet.add b acc) else acc) ); auto. reflexivity. intros. rewrite 2 (sameclass_equiv' _ _ H). reflexivity. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)