Depth r←≡y

r is a natural describing the depth of y: