Ensure that even bottoming functions have an unfolding
The payload of this change is to ensure that a bottoming function still has an unfolding, just one with an UnfoldingGuidance of UnfoldNever. Previously it was getting an unfolding of NoUnfolding. I don't think that was really /wrong/, but it was inconsistent with the general principle of giving everthing an unfoding if we know it. And it seems tideier this way.
Showing with 26 additions and 20 deletions