--- a/Quot/QuotSum.thy	Fri Jan 08 14:43:30 2010 +0100
+++ b/Quot/QuotSum.thy	Fri Jan 08 15:02:12 2010 +0100
@@ -82,4 +82,22 @@
   apply(rule sum_fun_fun[OF q1 q2])
   done
 
-end
\ No newline at end of file
+lemma sum_map_id[id_simps]: "sum_map id id \<equiv> id"
+  apply (rule eq_reflection)
+  apply (rule ext)
+  apply (case_tac x)
+  apply (auto)
+  done
+
+lemma sum_rel_eq[id_simps]: "sum_rel op = op = \<equiv> op ="
+  apply (rule eq_reflection)
+  apply (rule ext)+
+  apply (case_tac x)
+  apply auto
+  apply (case_tac xa)
+  apply auto
+  apply (case_tac xa)
+  apply auto
+  done
+
+end