diff -r 1bf4337919d3 -r 3e7a6ec549d1 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Thu Jan 21 09:55:05 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Thu Jan 21 10:55:09 2010 +0100
@@ -186,14 +186,19 @@
   using a b c
   by (lifting int_induct_raw)
 
-lemma ex1tst: "\<exists>! (x :: nat \<times> nat) \<in> Respects (op \<approx>). True"
+lemma ex1tst: "Bexeq (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)"
 sorry
 
-lemma ex1tst': "\<exists>! (x :: my_int). True"
+lemma ex1tst': "\<exists>! (x :: my_int). x = x"
 apply(lifting ex1tst)
+
+apply injection
+apply (rule quot_respect(9))
+apply (rule Quotient_my_int)
+
 apply(cleaning)
-apply simp
-sorry
+apply (simp add: ex1_prs[OF Quotient_my_int])
+done
 
 lemma ho_tst: "foldl my_plus x [] = x"
 apply simp