map length (tiers :: [[ NoDup Nat2 ]]) = [1,1,1,2] length (list :: [ NoDup Nat2 ]) = 5 allUnique (list :: [ NoDup Nat2 ]) = True ratioRepetitions (list :: [ NoDup Nat2 ]) = 0 % 1 tiers :: [NoDup Nat2] = [ [NoDup []] , [NoDup [0]] , [NoDup [1]] , [ NoDup [0,1] , NoDup [1,0] ] ]