--- a/IntEx.thy	Fri Nov 27 04:02:20 2009 +0100
+++ b/IntEx.thy	Fri Nov 27 07:00:14 2009 +0100
@@ -164,8 +164,12 @@
 apply simp
 done
 
+lemma map_prs: "map REP_my_int (map ABS_my_int x) = x"
+sorry
+
 lemma "foldl PLUS x [] = x"
 apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *})
+apply (simp_all only: map_prs)
 sorry
 
 (*