Negative4.agda:5,6-11
NSPos is not strictly positive, because it occurs to the left of an
arrow in the type of the constructor c in the definition of NSPos.