des_indefinite_description

[mdokomath]

Adds a tactic for easier work with constrictive_indefinite_description, which I needed reasonably often in a couple of my recent projects.

To me, the tactic has a distinct des_something feel about it.

See if the addition of it to Hahn makes sense.