BadInductionRecursion2.agda:7,1-12,19
D is not strictly positive, because it occurs
to the left of an arrow
in the first clause
in the definition of D′, which occurs
in the type of the constructor d
in the definition of D.
