Start fleshing out framework for proof
Lemmata for heap domain restriction
Lemmata for address translation