--- a/FIXME-TODO	Thu Dec 17 17:59:12 2009 +0100
+++ b/FIXME-TODO	Sat Dec 19 22:04:34 2009 +0100
@@ -14,14 +14,21 @@
 
 - Handle theorems that include Ball/Bex
 
-- quotient_respects and preserves in a natural form.
+- user should be able to give quotient_respects and 
+  preserves theorems in a more natural form.
 
+- the test in the (_, Const _) needs to be fixed
 
 Lower Priority
 ==============
 
 - accept partial equvalence relations
 
+- what happens if the original theorem contains bounded
+  quantifiers? can such theorems be lifted? If not, would 
+  it help if we introduced separate Bex and Ball constants
+  for quotienting?
+
 - inductions from the datatype package have a strange
   order of quantifiers in assumptions.