d = (_t1::forall {k} {a :: k}. D a)
()