Proof step 4 from proof crash-neutral-get (previous step)

key = datakey(ino, pageno), key ∈ pcache ⊦ ⟨let pe = pcache[key] in {buf := pe.page; boolvar := true}; err := ESUCCESS⟩ true

Heuristic symbolic execution applied rule let right

Proof step 5:
key = datakey(ino, pageno), pe = pcache[key], key ∈ pcache ⊦ ⟨buf := pe.page; boolvar := true; err := ESUCCESS⟩ true
Proof step 8:
key = datakey(ino, pageno), key ∈ pcache ⊦ key ∈ pcache