`unfold id n` tactic

[lambdacalculator]

Given that one of the possible witnesses is unfold(id,n,witness1,...,witnessn) (where the second n should really be k), wouldn't it make sense to have a tactic unfold id n, so that it wouldn't be necessary to litter one's specifications with names just so that specification clauses could be unfolded? I've often wished I had this ability when a search doesn't succeed: it would allow me to work backwards to find where the search is failing without having to redo my specification by adding names to all the clauses that might be involved.

[chaudhuri]

Seems reasonable. Thanks for the suggestion. I'll take a crack at it RSN.