FIXME-TODO
changeset 753 544b05e03ec0
parent 746 5ef8be0175f6
child 760 c1989de100b4
equal deleted inserted replaced
752:17d06b5ec197 753:544b05e03ec0
    45   Call it 'quotient_type'
    45   Call it 'quotient_type'
    46 
    46 
    47 - Maybe quotient and equiv theorems like the ones for
    47 - Maybe quotient and equiv theorems like the ones for
    48   [QuotList, QuotOption, QuotPair...] could be automatically
    48   [QuotList, QuotOption, QuotPair...] could be automatically
    49   proven?
    49   proven?
       
    50 
       
    51 - Examples: Finite multiset.