New lemma about map over merging graphs.
Add new Label form to the statement AST.
Getting into a tangle with hidag properties.
Syntax for (reflexive and) transitive closure of eval.
Start of proofs about sanity of labelling.
Almost done with "sanity of labelling" theorems.
Finish bisimulation result for strip_label equivalence.

naiveGraph is broken because of the presence of labels, but I'm not
sure I care a great deal.