BadInductionRecursion3.err

BadInductionRecursion3.agda:13,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 second clause in the definition of D′, which occurs in the type
of the constructor d in the definition of D.