# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260795548 -3600
# Node ID df962ca75ffa825bf834233da7e6d40071e7df28
# Parent  7e19c4b3ab0f1565b29f5faebd7bc2fb9fa716bd# Parent  76e34dd930f68f8255b0941ff55918ea4872bb4b
merge

diff -r 7e19c4b3ab0f -r df962ca75ffa FIXME-TODO
--- a/FIXME-TODO	Mon Dec 14 13:58:51 2009 +0100
+++ b/FIXME-TODO	Mon Dec 14 13:59:08 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?