map length (tiers :: [[ NoDup Nat ]])  =  [1,1,1,3,3,5,11,13,19,27,57,65,...]

length (list :: [ NoDup Nat ])  =  Infinity

allUnique (list :: [ NoDup Nat ])  =  True

ratioRepetitions (list :: [ NoDup Nat ])  =  0 % 1

tiers :: [NoDup Nat]  =
  [ [NoDup []]
  , [NoDup [0]]
  , [NoDup [1]]
  , [ NoDup [0,1]
    , NoDup [1,0]
    , NoDup [2]
    ]
  , [ NoDup [0,2]
    , NoDup [2,0]
    , NoDup [3]
    ]
  , [ NoDup [0,3]
    , NoDup [1,2]
    , NoDup [2,1]
    , NoDup [3,0]
    , NoDup [4]
    ]
  , [ NoDup [0,1,2]
    , NoDup [0,2,1]
    , NoDup [0,4]
    , NoDup [1,0,2]
    , NoDup [1,2,0]
    , NoDup [1,3]
    , NoDup [2,0,1]
    , NoDup [2,1,0]
    , NoDup [3,1]
    , NoDup [4,0]
    , NoDup [5]
    ]
  , [ NoDup [0,1,3]
    , NoDup [0,3,1]
    , NoDup [0,5]
    , NoDup [1,0,3]
    , NoDup [1,3,0]
    , NoDup [1,4]
    , NoDup [2,3]
    , NoDup [3,0,1]
    , NoDup [3,1,0]
    , NoDup [3,2]
    , NoDup [4,1]
    , NoDup [5,0]
    , NoDup [6]
    ]
  , [ NoDup [0,1,4]
    , NoDup [0,2,3]
    , NoDup [0,3,2]
    , NoDup [0,4,1]
    , NoDup [0,6]
    , NoDup [1,0,4]
    , NoDup [1,4,0]
    , NoDup [1,5]
    , NoDup [2,0,3]
    , NoDup [2,3,0]
    , NoDup [2,4]
    , NoDup [3,0,2]
    , NoDup [3,2,0]
    , NoDup [4,0,1]
    , NoDup [4,1,0]
    , NoDup [4,2]
    , NoDup [5,1]
    , NoDup [6,0]
    , NoDup [7]
    ]
  , [ NoDup [0,1,5]
    , NoDup [0,2,4]
    , NoDup [0,4,2]
    , NoDup [0,5,1]
    , NoDup [0,7]
    , NoDup [1,0,5]
    , NoDup [1,2,3]
    , NoDup [1,3,2]
    , NoDup [1,5,0]
    , NoDup [1,6]
    , NoDup [2,0,4]
    , NoDup [2,1,3]
    , NoDup [2,3,1]
    , NoDup [2,4,0]
    , NoDup [2,5]
    , NoDup [3,1,2]
    , NoDup [3,2,1]
    , NoDup [3,4]
    , NoDup [4,0,2]
    , NoDup [4,2,0]
    , NoDup [4,3]
    , NoDup [5,0,1]
    , NoDup [5,1,0]
    , NoDup [5,2]
    , NoDup [6,1]
    , NoDup [7,0]
    , NoDup [8]
    ]
  , [ NoDup [0,1,2,3]
    , NoDup [0,1,3,2]
    , NoDup [0,1,6]
    , NoDup [0,2,1,3]
    , NoDup [0,2,3,1]
    , NoDup [0,2,5]
    , NoDup [0,3,1,2]
    , NoDup [0,3,2,1]
    , NoDup [0,3,4]
    , NoDup [0,4,3]
    , NoDup [0,5,2]
    , NoDup [0,6,1]
    , NoDup [0,8]
    , NoDup [1,0,2,3]
    , NoDup [1,0,3,2]
    , NoDup [1,0,6]
    , NoDup [1,2,0,3]
    , NoDup [1,2,3,0]
    , NoDup [1,2,4]
    , NoDup [1,3,0,2]
    , NoDup [1,3,2,0]
    , NoDup [1,4,2]
    , NoDup [1,6,0]
    , NoDup [1,7]
    , NoDup [2,0,1,3]
    , NoDup [2,0,3,1]
    , NoDup [2,0,5]
    , NoDup [2,1,0,3]
    , NoDup [2,1,3,0]
    , NoDup [2,1,4]
    , NoDup [2,3,0,1]
    , NoDup [2,3,1,0]
    , NoDup [2,4,1]
    , NoDup [2,5,0]
    , NoDup [2,6]
    , NoDup [3,0,1,2]
    , NoDup [3,0,2,1]
    , NoDup [3,0,4]
    , NoDup [3,1,0,2]
    , NoDup [3,1,2,0]
    , NoDup [3,2,0,1]
    , NoDup [3,2,1,0]
    , NoDup [3,4,0]
    , NoDup [3,5]
    , NoDup [4,0,3]
    , NoDup [4,1,2]
    , NoDup [4,2,1]
    , NoDup [4,3,0]
    , NoDup [5,0,2]
    , NoDup [5,2,0]
    , NoDup [5,3]
    , NoDup [6,0,1]
    , NoDup [6,1,0]
    , NoDup [6,2]
    , NoDup [7,1]
    , NoDup [8,0]
    , NoDup [9]
    ]
  , [ NoDup [0,1,2,4]
    , NoDup [0,1,4,2]
    , NoDup [0,1,7]
    , NoDup [0,2,1,4]
    , NoDup [0,2,4,1]
    , NoDup [0,2,6]
    , NoDup [0,3,5]
    , NoDup [0,4,1,2]
    , NoDup [0,4,2,1]
    , NoDup [0,5,3]
    , NoDup [0,6,2]
    , NoDup [0,7,1]
    , NoDup [0,9]
    , NoDup [1,0,2,4]
    , NoDup [1,0,4,2]
    , NoDup [1,0,7]
    , NoDup [1,2,0,4]
    , NoDup [1,2,4,0]
    , NoDup [1,2,5]
    , NoDup [1,3,4]
    , NoDup [1,4,0,2]
    , NoDup [1,4,2,0]
    , NoDup [1,4,3]
    , NoDup [1,5,2]
    , NoDup [1,7,0]
    , NoDup [1,8]
    , NoDup [2,0,1,4]
    , NoDup [2,0,4,1]
    , NoDup [2,0,6]
    , NoDup [2,1,0,4]
    , NoDup [2,1,4,0]
    , NoDup [2,1,5]
    , NoDup [2,4,0,1]
    , NoDup [2,4,1,0]
    , NoDup [2,5,1]
    , NoDup [2,6,0]
    , NoDup [2,7]
    , NoDup [3,0,5]
    , NoDup [3,1,4]
    , NoDup [3,4,1]
    , NoDup [3,5,0]
    , NoDup [3,6]
    , NoDup [4,0,1,2]
    , NoDup [4,0,2,1]
    , NoDup [4,1,0,2]
    , NoDup [4,1,2,0]
    , NoDup [4,1,3]
    , NoDup [4,2,0,1]
    , NoDup [4,2,1,0]
    , NoDup [4,3,1]
    , NoDup [4,5]
    , NoDup [5,0,3]
    , NoDup [5,1,2]
    , NoDup [5,2,1]
    , NoDup [5,3,0]
    , NoDup [5,4]
    , NoDup [6,0,2]
    , NoDup [6,2,0]
    , NoDup [6,3]
    , NoDup [7,0,1]
    , NoDup [7,1,0]
    , NoDup [7,2]
    , NoDup [8,1]
    , NoDup [9,0]
    , NoDup [10]
    ]
  , ...
  ]