'type:nat+nat '+{True}
     : Set
{True}+{True}+{True}
     : Set
nat+{True}+{True}
     : Set