∀(r : { z : Natural }) → { x : { y : Natural, z : Natural } }