--- a/Quot/Examples/FSet.thy	Tue Jan 26 13:53:56 2010 +0100
+++ b/Quot/Examples/FSet.thy	Tue Jan 26 13:58:28 2010 +0100
@@ -398,4 +398,23 @@
 apply(lifting test3)
 done
 
+lemma test4: "\<forall> (x :: 'a list, y, z) \<in> Respects(
+  prod_rel (op \<approx>) (prod_rel (op \<approx>) (op \<approx>))
+). x = y \<and> y = z"
+sorry
+
+lemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)"
+apply (lifting test4)
+sorry
+
+lemma test5: "\<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>))
+). x = y \<and> y = z"
+sorry
+
+lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y, z). x = y \<and> y = z)"
+apply (lifting test5)
+sorry
+
+
 end