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

   440 sorry

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

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

   443 done

   444 

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

   446 sorry

   447 

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

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

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

   451 defer

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

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

   454 sorry

   455 

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

   457 sorry

   458 

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

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

   461 sorry