type-natural Type-level well-kinded peano natural numbers and singletons with proofs of their properties.