dfns should have IDs

[bakkot]

So they can be linked to instead of just getting the containing clause.

Especially after #441.