| author | Cezary Kaliszyk <kaliszyk@in.tum.de> | 
| Mon, 14 Dec 2009 13:57:39 +0100 | |
| changeset 747 | 76e34dd930f6 | 
| parent 746 | 5ef8be0175f6 (diff) | 
| parent 745 | 33ede8bb5fe1 (current diff) | 
| child 749 | df962ca75ffa | 
--- a/FIXME-TODO Mon Dec 14 10:19:27 2009 +0100 +++ b/FIXME-TODO Mon Dec 14 13:57:39 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?