[supporting lemma]: initialized should imply can_write
stilltracy opened this issue · 1 comments
stilltracy commented
A lemma stating sth. like "initialized m x -> can_write m x" is needed when proving consistent_mem_vals & consistent_mem_vals'.
mansky1 commented
We also need "consistent m", but this is now proved.