Negative5.agda:3,6-11
The datatype Funny is not strictly positive, because it occurs
negatively in the constructor .Negative5.funny of Funny