I started thinking about this more in relation to double dereferences, etc and realized this should be some kind of recursive process because pointers can be refined at every level.
For example

p → {&q, &r}
q → {&x, &y}
r → {&z, &w}
x → {1}
y → {2}
z → {1}
w → {3}

Assuming **p == 2 should refine p → {&q} and q → {&y}.
Seems like Mem should just recurse (while refining the pointer) and Var would be the base case.

Or perhaps not be so ambitious and handle nested dereferences... It's surprisingly tricky to get right even in very simple theoretical setting (the unassume paper appendix on pointers). We spent over an hour with Vesal trying to get it right in a semi-general case (where lvalues are sequences of derefs ending with a variable, so no arbitrary expressions in dereference, nor offsets). The formal definition is also very inefficient in subtle ways because the AST of such lvalues is in the wrong direction compared to the order of dereferencing pointers (which happens from inside out).
It's worth revisiting separately to not block this PR.

I have now somewhat generalized the handling here. Recursive pointers etc are not considered yet, we can do this in a separate PR if we want to be ambitious.