lemma dlist_ext

--- a/src/HOL/Library/Dlist.thy	Wed Apr 21 21:11:26 2010 +0200
+++ b/src/HOL/Library/Dlist.thy	Thu Apr 22 09:30:36 2010 +0200
@@ -47,6 +47,11 @@
   show "[] \<in> ?dlist" by simp
 qed
 
+lemma dlist_ext:
+  assumes "list_of_dlist xs = list_of_dlist ys"
+  shows "xs = ys"
+  using assms by (simp add: list_of_dlist_inject)
+
 
 text {* Formal, totalized constructor for @{typ "'a dlist"}: *}