Function obeys_cmp_concrete_eq 

pub open spec fn obeys_cmp_concrete_eq<T: Ord>() -> bool

{ forall |v1: T, v2: T| v1.cmp_spec(&v2) is Equal <==> v1 == v2 }

Whether the type’s cmp spec matches structural equality, i.e., whether v1.cmp(&v2) is Equal <==> v1 == v2.