Filling out correctness proof in metatheory. Still needs a bit more work (and discussion of order invariants)