265 | | For the equality store, my rough plan is to handle both issues (preferring compactness over transparency) in one step: before writing out the equalities in the store, for each ~~root (i.e. variable not in the domain of the substitution), I'll compact that root's equality constraints by finding a minimum spanning tree of the weighted fully connected graph in which each node is a variable in the substitution domain whose mapping extends that root and each weight is the total `typeSize` of the union of their extension minus the intersection of their extension and emit the MST's edges as the simplified equality constraints~~. |

266 | | |

267 | | I haven't considered the `Lacks` store yet. |

| 265 | For the equality store, my rough plan is to handle both issues (preferring compactness over transparency) in one step: before writing out the equalities in the store, for each implicit variable root, I'll compact that root's equality constraints by finding a minimum spanning tree of the weighted fully connected graph in which each node is a variable in the substitution domain whose mapping extends that root and each weight is the total `typeSize` of the union of their extension minus the intersection of their extension and emit the MST's edges as the simplified equality constraints. For explicit variable roots and the empty set root, no processing is strictly necessary, but the same algorithm would compact their representation, I think. |

| 266 | |

| 267 | I haven't considered the `Lacks` store yet. I haven't convinced myself that a greedy algorithm would find the minimal way to express a set form. |