proposition: Lemma class_of_In_MapsTo : forall `{WF} x z, NumMap.MapsTo x z (p t) -> NumSet.In x (class_of t z).
proof: Proof. intros t Hwf x z H. unfold class_of. NumSetProps.set_iff. right. unfold class_of'. assert (NumMap.Equal (p t) (NumMap.add x z (NumMap.remove x (p t)))). intro y. find_analyse; completer idtac; find_tac. destruct H2. find_tac. elim H1. rewrite NumMapProps.remove_in_iff. destruct (eq_num_dec x y); firstorder. destruct H2. firstorder. rewrite Z.fold_Equal; ti_auto. rewrite NumMapProps.fold_add; ti_auto. clear H0. case_eq (fst (equiv t z x)); case_eq (fst (equiv t z z)); intros; simpl. NumSetProps.set_iff. left. num_prop. reflexivity. apply equiv_reflexive_false in H0; auto;tauto_false. apply MapsTo_sameclass in H. exfalso. symmetry in H. rewrite <- sameclass_equiv in H. congruence. apply equiv_reflexive_false in H0; auto; tauto_false. repeat intro; subst. case (fst (equiv t z y) && fst (equiv t z y0)); rewrite H3; reflexivity. repeat intro; subst. repeat match goal with |- context [fst (equiv ?t ?x ?y)] => case (fst (equiv t x y)) end; simpl;try NumSetProps.setdec. rewrite NumMapProps.remove_in_iff. intro. tauto_false. repeat intro; subst. case (fst (equiv t z y) && (fst (equiv t z y0))); rewrite H3; reflexivity. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)