Unification of Nat and Naturals

This patch removes the separate kind 'Nat' and enables promotion of type 'Natural' for using as type literal.

Now the following code will be successfully type-checked:

data C = MkC Natural
type CC = MkC 1

Before this change, we had to create the separate type for promotion

data C = MkC Natural
data CP = MkCP Nat
type CC = MkCP 1

But CP is uninhabited in terms.

For backward compatibility type synonym Nat has been made:

type Nat = Natural

The user's documentation and tests have been updated.

WIP since one of the tests stuck for some reason.