--- a/Quot/Examples/FSet.thy	Tue Dec 08 22:24:24 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 22:26:01 2009 +0100
@@ -444,4 +444,22 @@
 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)
 sorry
 
+lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
+sorry
+
+lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))"
+apply(lifting_setup hard)
+defer
+apply(injection)
+apply(subst babs_prs)
+defer defer
+apply(subst babs_prs)
+defer defer
+apply(subst babs_prs)
+defer defer
+apply(subst babs_prs)
+defer defer
+apply(tactic {* lambda_prs_tac @{context} 1 *})
+(* Until here is ok *)
+apply(cleaning)
 end