Correct proof of imap_merge_graph result.
Slight progress with renaming invariance proof for graphOf.