Kinded Proofs
Kinds allow the program to setup a "cleanroom" environment for the type system. The canonical example of polykinding is for the Unit kind.
The International System of Units defines a unit as a Number combined with a Unit. In LSTS this can be modelled as the number being a Term and the unit being a Unit. The SI system additionally defines several units as "base units". All units that are not base units can be written as a compound of base units. Examples of base units are Seconds or Metres. Examples of non-base units are Joules or Teslas.
In LSTS it is convenient to mark base units as normal. A normal Type can be preferred during type conversion. For example, if a unit of Speed is multiplied by a unit of Time, it will result in a unit of Distance. When we look closer at these units we see that Speed is a unit of Distance over Time. It is only within this normal form that we can discover that Speed * Time = Distance.
Kinded Projection
If you want to work within a Kind and only within that Kind then you should use Kind Projection. A compound Type x: Real + Second can be narrowed into a Unit with double colon syntax: x :: Unit. This will leave the term with only the type Second, stripping the variable of its other associated Types.