Agda-2.3.2.2: test/fail/Negative1.err
Negative1.agda:3,6-7 D is not strictly positive, because it occurs to the left of an arrow in the type of the constructor lam in the definition of D.
Negative1.agda:3,6-7 D is not strictly positive, because it occurs to the left of an arrow in the type of the constructor lam in the definition of D.