diff -r ea123790121b -r 82cc2aeb7d13 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Wed May 15 12:10:39 2013 +0200
@@ -57,7 +57,7 @@
   by (auto iff: fun_eq_iff)
 qed 
 
-lemma list_reflp[reflexivity_rule]:
+lemma reflp_list_all2[reflexivity_rule]:
   assumes "reflp R"
   shows "reflp (list_all2 R)"
 proof (rule reflpI)
@@ -67,16 +67,20 @@
     by (induct xs) (simp_all add: *)
 qed
 
-lemma list_left_total[reflexivity_rule]:
-  assumes "left_total R"
-  shows "left_total (list_all2 R)"
-proof (rule left_totalI)
-  from assms have *: "\<And>xs. \<exists>ys. R xs ys" by (rule left_totalE)
-  fix xs
-  show "\<exists> ys. list_all2 R xs ys"
-    by (induct xs) (simp_all add: * list_all2_Cons1)
-qed
+lemma left_total_list_all2[reflexivity_rule]:
+  "left_total R \<Longrightarrow> left_total (list_all2 R)"
+  unfolding left_total_def
+  apply safe
+  apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
+done
 
+lemma left_unique_list_all2 [reflexivity_rule]:
+  "left_unique R \<Longrightarrow> left_unique (list_all2 R)"
+  unfolding left_unique_def
+  apply (subst (2) all_comm, subst (1) all_comm)
+  apply (rule allI, rename_tac zs, induct_tac zs)
+  apply (auto simp add: list_all2_Cons2)
+  done
 
 lemma list_symp:
   assumes "symp R"
@@ -102,7 +106,7 @@
 
 lemma list_equivp [quot_equiv]:
   "equivp R \<Longrightarrow> equivp (list_all2 R)"
-  by (blast intro: equivpI list_reflp list_symp list_transp elim: equivpE)
+  by (blast intro: equivpI reflp_list_all2 list_symp list_transp elim: equivpE)
 
 lemma right_total_list_all2 [transfer_rule]:
   "right_total R \<Longrightarrow> right_total (list_all2 R)"