# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260795384 -3600
# Node ID 5ef8be0175f637dada2c83f2be5c1d4be0f51a27
# Parent  198ff5781844c0359ac55e3204400c8a180eca04
FIXME/TODO.

diff -r 198ff5781844 -r 5ef8be0175f6 FIXME-TODO
--- a/FIXME-TODO	Sun Dec 13 02:47:47 2009 +0100
+++ b/FIXME-TODO	Mon Dec 14 13:56:24 2009 +0100
@@ -43,3 +43,7 @@
 
 - We shouldn't use the command 'quotient' as this shadows Larry's quotient.
   Call it 'quotient_type'
+
+- Maybe quotient and equiv theorems like the ones for
+  [QuotList, QuotOption, QuotPair...] could be automatically
+  proven?