diff -r 7ba2fc25c6a3 -r 9b1ad366827f FIXME-TODO
--- a/FIXME-TODO	Fri Dec 04 14:11:20 2009 +0100
+++ b/FIXME-TODO	Fri Dec 04 14:35:36 2009 +0100
@@ -12,7 +12,9 @@
   theorem cannot be lifted) / proper diagnostic 
   messages for the user
 
-- Ask Peter and Michael for challenging examples 
+- Ask Peter and Michael for challenging examples
+  And for examples where it is useful to lift types
+  over a relation being only a partial equivalence