Deprecate `inspect` function in favour of new `with ... in` construct

[MatthewDaggitt]

@gallais added the inspect idiom as a first class language construct in Agda 2.6.2. We should consider using it in the library to simplify our code, and possibly deprecating the old inspect function to encourage other people to migrate as well.

[ajrouvoet]

I hope this would also (eventually) get rid of the imported [_] from PropositionalEquality which clashes with list singletons and others.

[MatthewDaggitt]

You're not the only one who has expressed this wish, @jamesmckinna also mentioned this. It will be deprecated first, but yes eventually it'll be removed.

[jamesmckinna]

Suggest closing this now, after the merge of #1930, notwithstanding the issues of strictness of inspect vs. laziness of with ... in ... raised by agda#5833