Unsilence deprecation warning regarding list lemmas.

I think having our own (direct) version of this two line proof (instead of going via an equivalent to a stdlib def) is less problematic than missing out on other deprecation warnings.

changed the description

Should we add a note to go back to the old proof once we require Coq 8.20?

I don't think I care enough to change it back then

mentioned in commit 6a0896a2

merged