--- a/Quot/Examples/FSet.thy	Mon Dec 07 21:21:57 2009 +0100
+++ b/Quot/Examples/FSet.thy	Mon Dec 07 21:25:49 2009 +0100
@@ -436,5 +436,28 @@
 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
 done
 
+lemma ttt: "((op @) x ((op #) e [])) = (((op #) e x))"
+sorry
+lemma "(FUNION x (INSERT e EMPTY)) = ((INSERT e x))"
+apply (tactic {* lift_tac @{context} @{thm ttt} 1 *})
+done
+
+lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))"
+sorry
+
+lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"
+apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *})
+apply(tactic {* regularize_tac @{context} 1 *})
+defer
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1*})
+(* apply(tactic {* clean_tac @{context} 1 *}) *)
+sorry
+
+lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
+sorry
+
+lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))"
+(* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)
+sorry
 
 end