BadInductionRecursion1.agda:7,1-12,14
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.
