feat: verify all and any for hash maps

[jt0202]

This PR extends the all/any functions from hash sets to hash maps and dependent hash maps and verifies them.

[TwoFX]

Given that we have recently got any and all on iterators (#10686) and hash map iterators are coming up (#10761), the question arises: should we define m.all p on a hash map m to be m.iter.all p (or, even more radical, not provide it at all and expect users to write m.iter.all p themselves)?

And hopefully if the right lemmas about HashMap.iter and Iter.any exist, all any lemmas you might want on hash maps fall right out?

@datokrat, any thoughts?

[jt0202]

Given that we have recently got any and all on iterators (#10686) and hash map iterators are coming up (#10761), the question arises: should we define m.all p on a hash map m to be m.iter.all p (or, even more radical, not provide it at all and expect users to write m.iter.all p themselves)?

This would also work for me and then we can close this one. I feel like it would be more comfortable for the user to still have the custom any/all function as the iterator seems to me like an implementation detail.

[datokrat]

@datokrat, any thoughts?

I think this will work -- however, one should perhaps run a benchmark comparing the iterators' any and the current HashMap.any. Because the compiler is still sometimes struggling to optimize iterator for-in (used to implement any), there might be a slowdown.

If it turns out that there is still a performance benefit to implementing HashMap.any separately, another way to go would be to prove that it coincides with Iter.any and then transport all the lemmas along that equality.