In Python 3, dict value iterators aren't deterministic between runs, which causes nondeterministic definition output order. Some L4V proofs are sensitive to this order. Use sorted keys to guarantee order when iterating over values.