--- a/Attic/FIXME-TODO	Tue Jun 21 23:59:36 2011 +0900
+++ b/Attic/FIXME-TODO	Wed Jun 22 04:49:56 2011 +0900
@@ -18,6 +18,12 @@
 - The user should be able to give quotient_respects and
   preserves theorems in a more natural form.
 
+- Provide syntax for different names of Abs and Rep functions
+  in a similar way to typedef
+
+    typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
+      morphisms list_of_dlist Abs_dlist
+
 Lower Priority
 ==============