BadInductionRecursion2.err

BadInductionRecursion2.agda:8,8-9
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.