--- a/Quot/Examples/FSet.thy	Thu Dec 10 10:36:05 2009 +0100
+++ b/Quot/Examples/FSet.thy	Thu Dec 10 10:54:45 2009 +0100
@@ -343,13 +343,14 @@
 apply(rule list_eq_refl)
 done
 
-lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
+lemma ttt3: "(\<lambda>x. ((op @) x (e # []))) = (op #) e"
 sorry
 
-
-lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))"
-(* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)
-sorry
+lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = INSERT e"
+apply(lifting ttt3)
+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