a variant of distinct_map already exists in List.thy, so we are not going to do our own