Slightly adjust imap definition.

New form allows for maps that move identically numbered but otherwise
different actions to be renumbered apart. loop_to_graph would never
construct such actions (each action it produces get a different
number), but it's still nice to extend the strength of the renumbering
theorem.
Prove that loop_to_graph produces well-formed graphs.

Adjust the definition of add_action slightly to make this go through:
add_action now does nothing if the action its asked to add is already
present in the graph; again this wouldn't happen in loop_to_graph, but
its nice to have well-behaved primitives.