paraphrasing equality

--- a/src/HOL/List.thy	Fri Mar 30 16:18:59 2007 +0200
+++ b/src/HOL/List.thy	Fri Mar 30 16:19:00 2007 +0200
@@ -1601,6 +1601,10 @@
   apply (case_tac y, auto)
   done
 
+lemma list_all2_eq:
+  "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
+  by (induct xs ys rule: list_induct2') auto
+
 
 subsubsection {* @{text foldl} and @{text foldr} *}