--- a/Quot/Examples/IntEx.thy	Thu Jan 21 09:02:04 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Thu Jan 21 09:55:05 2010 +0100
@@ -186,6 +186,15 @@
   using a b c
   by (lifting int_induct_raw)
 
+lemma ex1tst: "\<exists>! (x :: nat \<times> nat) \<in> Respects (op \<approx>). True"
+sorry
+
+lemma ex1tst': "\<exists>! (x :: my_int). True"
+apply(lifting ex1tst)
+apply(cleaning)
+apply simp
+sorry
+
 lemma ho_tst: "foldl my_plus x [] = x"
 apply simp
 done