No large elimination

def Unit : Type := sum
 'tt
end

def Bool : Type := sum
  'true
  'false
end

def LandOrSea : Type := sum
  'land
  'sea
end

def paul-revere (method : LandOrSea) : Type := match method
  'land => Unit
  'sea => Bool
end