Add various specs for HashSet, FSet, and iterators (ranges, filter_map, rev)

[Lysxia]

• Also strengthen the spec of filter

Note: the spec for Borrow is required for HashSet::contains

[jhjourdan]

This contains quite a lot of new specifications that need to be discussed.

For example, I am not so sure the spec for double ended iterators is the one we want, because it does not say anything about how the forward and the backward relation interact.

[Lysxia]

The current spec for double ended iterators is at least enough for reasoning about simple and common for loops and .collect().

My understanding is that we're not too happy with the iterator specs as a whole (we'd like either better handling of existentials or to rework the specs to make proofs easier) so I'm wary of putting too much work into iterator specs up front. My approach is more to develop just what is needed by examples I come across. It's better to have some specs than none especially for iterators since Creusot can't translate for loops without specs.

[jhjourdan]

We are going to merge this as soon as this is rebased.