--- a/QuotMain.thy	Wed Oct 14 18:13:16 2009 +0200
+++ b/QuotMain.thy	Thu Oct 15 10:25:23 2009 +0200
@@ -427,7 +427,7 @@
         val rec_term = regularise t' rty rel lthy2;
         val lam_term = Term.lambda_name (x, v) rec_term
       in
-        Const(@{const_name "All"}, at) $ lam_term
+        Const(@{const_name "Ex"}, at) $ lam_term
       end
   | ((Const (@{const_name "Ex"}, at)) $ P) =>
       let
@@ -1147,21 +1147,6 @@
 
 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
 
-(* TODO: the following 2 lemmas should go to quotscript.thy after all are done *)
-lemma RIGHT_RES_FORALL_REGULAR:
-  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
-  shows "All P ==> Ball R Q"
-  using a
-  apply (metis COMBC_def Collect_def Collect_mem_eq a)
-  done
-
-lemma LEFT_RES_FORALL_REGULAR:
-  assumes a: "!x. (R x \<and> (Q x --> P x))"
-  shows "Ball R Q ==> All P"
-  using a
-  apply (metis COMBC_def Collect_def Collect_mem_eq a)
-  done
-
 prove {*
  Logic.mk_implies
    ((prop_of li),
@@ -1177,6 +1162,19 @@
   apply (assumption)
   done
 
+ML {* val li = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
+
+prove card1_suc_r: {*
+ Logic.mk_implies
+   ((prop_of li),
+   (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
+  apply (simp only: equiv_res_forall[OF equiv_list_eq])
+  apply (simp only: equiv_res_exists[OF equiv_list_eq])
+  done
+
+thm card1_suc
+ML {* @{thm card1_suc_r} OF [li] *}
+
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
 *}
@@ -1234,8 +1232,9 @@
 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
-(*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} @{context}) *}
-local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
+thm card1_suc_r
+ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc_r} @{context}) *}
+(*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
 
 thm m1_lift
 thm leqi4_lift