Function obeys_cmp_deep_eq 

pub open spec fn obeys_cmp_deep_eq<T: Ord + DeepView>() -> bool

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

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