In the practice of deductive program verification, it is desirable to make proofs as automated as possible. Today, the best tools for that are SMT solvers, which are able to handle both first-order logic and linear arithmetic. However, SMT solvers are not well suited for inductive reasoning, which is often needed to deal with recursive data structures such as linked lists or trees. In this paper, we propose a technique for specifying and proving imperative programs manipulating pointer-based recursive data structures, which stays within reach of first-order provers. The idea is to map a recursive structure onto a flat integer-indexed sequence, in such a way that separation and frame properties can be expressed using only simple arithmetic relations. We illustrate this approach with two examples: an original variant of list reversal and Morris’s algorithm for constant-space traversal of a binary tree.