--- a/Quotient-Paper/Paper.thy	Fri Oct 15 15:24:19 2010 +0900
+++ b/Quotient-Paper/Paper.thy	Fri Oct 15 15:52:40 2010 +0900
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "Quotient"
+imports "Quotient" "Quotient_Syntax"
         "LaTeXsugar"
         "../Nominal/FSet"
 begin
@@ -62,6 +62,29 @@
          (id ---> rep_fset ---> abs_fset) op #"
   by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
 
+lemma concat_rsp_unfolded:
+  "\<lbrakk>list_all2 list_eq a ba; list_eq ba bb; list_all2 list_eq bb b\<rbrakk> \<Longrightarrow> list_eq (concat a) (concat b)"
+proof -
+  fix a b ba bb
+  assume a: "list_all2 list_eq a ba"
+  assume b: "list_eq ba bb"
+  assume c: "list_all2 list_eq bb b"
+  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+    fix x
+    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+      assume d: "\<exists>xa\<in>set a. x \<in> set xa"
+      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
+    next
+      assume e: "\<exists>xa\<in>set b. x \<in> set xa"
+      have a': "list_all2 list_eq ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a])
+      have b': "list_eq bb ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
+      have c': "list_all2 list_eq b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c])
+      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
+    qed
+  qed
+  then show "list_eq (concat a) (concat b)" by auto
+qed
+
 (*>*)