380 lemma [quot_respect]:

   381   "((op \<approx> ===> op \<approx> ===> op =) ===> prod_rel op \<approx> op \<approx> ===> op =) split split"

   382 apply(simp)

   383 done

   384 

   385 thm quot_preserve

   386 term split

   387 

   388 

   389 lemma [quot_preserve]:

   390   shows "(((abs_fset ---> abs_fset ---> id) ---> prod_fun rep_fset rep_fset ---> id) split) = split"

   391 apply(simp add: expand_fun_eq)

   392 apply(simp add: Quotient_abs_rep[OF Quotient_fset])

   393 done

   394 

   395 

   396 lemma test: "All (\<lambda>(x::'a list, y). x = y)"

   397 sorry

   398 

   399 lemma  "All (\<lambda>(x::'a fset, y). x = y)"

   400 apply(lifting test)

   401 apply(cleaning)

   402 thm all_prs

   403 apply(rule all_prs)

   404 apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1*})

   405 done

   406 

   407 lemma test2: "Ex (\<lambda>(x::'a list, y). x = y)"

   408 sorry

   409 

   410 lemma  "Ex (\<lambda>(x::'a fset, y). x = y)"

   411 apply(lifting test2)

   412 apply(cleaning)

   413 apply(rule ex_prs)

   414 apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1*})

   415 done

   416 

   417 ML {* @{term "Ex (\<lambda>(x::'a fset, y). x = y)"} *}

   418 

   419