diff -r 0aaeea9255f3 -r 6267ad688ea8 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Jan 26 14:08:47 2010 +0100
+++ b/Quot/Examples/FSet.thy	Tue Jan 26 14:48:25 2010 +0100
@@ -409,12 +409,20 @@
 
 lemma test5: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y) \<in> Respects(
   prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>)
-). x = y"
+). (op \<approx> ===> op \<approx>) x y"
 sorry
 
 lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y). x = y)"
 apply (lifting test5)
+done
+
+lemma test6: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y, z) \<in> Respects(
+  prod_rel (op \<approx> ===> op \<approx>) (prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>))
+). (op \<approx> ===> op \<approx>) x y \<and> (op \<approx> ===> op \<approx>) y z"
 sorry
 
+lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y, z). x = y \<and> y = z)"
+apply (lifting test6)
+done
 
 end