En sin forma, el tipo Nat representa una forma de codificar números naturales a nivel de tipo. Esto se usa, por ejemplo, para listas de tamaño fijo. Incluso puede hacer cálculos a nivel de tipo, por ejemplo, agregar una lista de Nelementos a una lista de Kelementos y recuperar una lista que se sabe...