Update NAG proofs to handle AssignVar with separate reads

This is follow up work from the change started in 65533aa.
Adjust single-step semantics to make relabelling easier.

New rule says

  (m0, IfStmt gd th el) --> (m0, Seq [Done; c])

where c is one of th or el, depending on how the guard evaluates.
The bogus insertion of a Done command (a Skip if you will) ensures
that when you create a nested graph on the left and a graph on the
right, you will end up with the same number of nodes.

On the left, you get a readAction corresponding to the expression
evaluation and one for the command. On the right you will get one for
the Done, and one for the command. The fact that the node on the right
for the Done will just contain an empty graph is neither here nor
there.