430 lemma ttt: "((op @) x ((op #) e [])) = (((op #) e x))"

   431 sorry

   432 lemma "(FUNION x (INSERT e EMPTY)) = ((INSERT e x))"

   433 apply (tactic {* lift_tac @{context} @{thm ttt} 1 *})

   434 done

   435 

   436 lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))"

   437 sorry

   438 

   439 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"

   440 apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *})

   441 apply(tactic {* regularize_tac @{context} 1 *})

   442 defer

   443 apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1*})

   444 (* apply(tactic {* clean_tac @{context} 1 *}) *)

   445 sorry

   446 

   447 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"

   448 sorry

   449 

   450 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))"

   451 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)

   452 sorry