--- a/Quot/Examples/FSet.thy	Thu Dec 10 11:19:34 2009 +0100
+++ b/Quot/Examples/FSet.thy	Thu Dec 10 12:25:12 2009 +0100
@@ -351,14 +351,23 @@
 apply(regularize)
 apply(auto simp add: cons_rsp)
 done
-
 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 hard)
 apply(regularize)
-apply(auto)
-sorry
+apply(rule fun_rel_id_asm)
+apply(subst babs_simp)
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(rule fun_rel_id_asm)
+apply(rule impI)
+apply(rule mp[OF eq_imp_rel[OF fset_equivp]])
+apply(drule fun_cong)
+apply(drule fun_cong)
+apply(assumption)
+done
+
+
 
 end