feat: `Std.Iter.toHashSet` (#12524)

This PR adds `Std.Iter.toHashSet` and variants.

Included: variants starting from both monadic and non-monadic iterators,
producing extensional and non-extensional hash sets and tree sets.

Lemmas are included, showing that `it.toHashSet ~m HashSet.ofList
it.toList` (equivalence of hash sets) and `it.toExtHashSet =
ExtHashSet.ofList it.toList` (equality of extensional hash sets).