-Frequently, it is more convenient to not talk about raw lists of bytes but about some higher-level representation of the bytes, and not care about how exactly that data is laid out in memory.
-For example, we might want to say that `ptr` points to `42` of type `i32` by saying `mem_own(ptr, 42i32)`.
-We can define a suitable `mem_own` as
-```
-mem_own<U>(ptr: Pointer, data: U) where List<Bytes>: TryInto<U> :=
- exists |bytes| bytes.try_into() == Ok(data) && mem_own(ptr, bytes)
-```
-Here, we (ab)use the `TryInto` trait to convert a properly laid out list of bytes into something of type `U`.
-The conversion fails, in particular, if the list does not have exactly the right length.
-If `U == List<Bytes>`, this is just the same as `mem_own_bytes`.
+**Update:** In a previous version I called this predicate `mem_own`. I decided that `points_to_owned` was actually easier to understand, and it also matches the standard terminology in the literature, so I switched to using that term instead. **/Update**