Negative3.agda:3,6-8
Mu is not strictly positive, because it occurs in an argument to a
bound variable in the type of the constructor inn in the definition
of Mu.