Two more minor theorems about list ranges.
Prove loop_to_graph is a fold, and *really* prove it produces wf graphs.

Previous commit only proved that add_action preserved well-formedness,
which is the heart of the issue of course, but not the claimed result.