Negative4.agda:5,6-11
The datatype NSPos is not strictly positive, because it occurs
negatively in the constructor .Negative4.c of NSPos