Just to clarify, what are the suggestions


Variant A:

1) twin (and similar ones: clone, copy, etc.) should change
      Result ~ Current
into
      Current = Current implies Result ~ Current

2) all containers should change postconditions like
      item (...) = value
into
      value = value implies item (...) = value


Variant B (similar to KL_TYPE.same_objects of Gobo):

1) twin (and similar ones: clone, copy, etc.) should change
      Result ~ Current
into
      safe_equal (Result, Current)
where
      safe_equal will do internally the checks of variant A (or use the code similar to KL_TYPE.same_objects)

2) all containers should change postconditions like
      item (...) = value
into
      safe_equal (item (...), value)


Variant C:

The compiler always treats NaN values as equal.


Variant D:

The compiler treats bit-wise identical NaN values as equal.