BadInductionRecursion1.err

BadInductionRecursion1.agda:8,8-9
D is not strictly positive, because it occurs in the first clause
in the definition of D′, which occurs to the left of an arrow in
the type of the constructor d in the definition of D.