pub open spec fn obeys_view_eq<T: PartialEq + View>() -> bool
{ &&& T::obeys_eq_spec() &&& forall |x: T, y: T| x.eq_spec(&y) <==> x@ == y@ }