Complete graphOf renaming lemma.
Progress with graphOf correctness proof, but...

Revision to model is going to be needed to record the fact that the
construction of the graph depends on "reads" of memory that aren't
apparent only in the Assign constructor. In particular, there are
reads that happen in the course of evaluating the guards of
if-statements and the like.
Revise action-graphs to allow actions with no writes.

Such actions don't do anything (they don't affect memory), but they
can record a dependence that we might otherwise miss out on. Adjust
the earlier datadeps theory so that it still works in the face of this
change. PseudoCProps broken.
Adjust PseudoC props theory for actions without writes.

Still doesn't build though.