Issue690.agda:14,6-7
D is not strictly positive, because it occurs in the second
argument to _≡_ in the type of the constructor abs in the
definition of D.