Stronger version of `gmap_core_id`.
To obtain CoreId m
where m : gmap K A
, the prior version requires CoreId
to hold for all values x : A
. The new version only requires it to hold for values that are in the map, i.e., with m !! i = Some x
.
Since the condition m !! i = Some x
is useless for type classes, I made a primed version gmap_core_id'
without that condition, and declared that as an instance.