proposition: Lemma sameclass_class_of : forall `{WF} x y , sameclass t x y <-> NumSet.In x (class_of t y).
proof: Proof. intros t Hwf x y. split; intros. - destruct H as [z H H']. assert (Hx := class_of_In_repr _ _ H). assert (Hy := class_of_In_repr _ _ H'). revert Hx Hy; unfold class_of; NumSetProps.set_iff; num_prop. intros [? |?] [? |?]; subst; auto. clear H. assert (h'' := class_of_In_repr' _ _ H'). unfold class_of in h''. revert h''. NumSetProps.set_iff. num_prop. intuition. rewrite <- (class_of_Equal_repr _ _ H'). auto. - unfold class_of in H. unfold class_of', class_of in H. revert H. NumSetProps.set_iff. num_prop. intros [? |?]. subst. reflexivity. induction (p t) using Z.map_induction_max. * assert (H1 := NumMap_Equal_Empty_empty _ t0 H0). setoid_rewrite (Z.fold_Equal _ _ _ H1) in H . rewrite (NumMapProps.fold_Empty (eqA := NumSet.Equal)) in H; ti_auto. clear - H Hwf. revert H. NumSetProps.set_iff. num_prop. intuition. subst. auto with map. * erewrite (Z.fold_Add_Above (eqA := NumSet.Equal)) in H; ti_auto. 2 : repeat intro; subst; destruct (fst (equiv t y y0) && fst (equiv t y y1)); try NumSetProps.setdec. case_eq (fst (equiv t y x0) && (fst (equiv t y e))); intros; cbn in *; rewrite H2 in *. 2 :apply IHt0_1; auto. revert H. NumSetProps.set_iff; num_prop. intros [? | [? | ?]]; num_prop; subst. + clear - H2 Hwf. bool_connectors; rewrite sameclass_equiv in H2;try symmetry; auto. intuition. + clear - H2 Hwf. bool_connectors; rewrite 2 sameclass_equiv in H2;try symmetry; auto. intuition. + apply IHt0_1. auto. Qed.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)