Discussed at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Outstanding.20equations.2C.20v1/near/478537706 . The tentative plan from Zoltan Kocsis is

" unify the planner and the transitive closure / duality computation, and compute one final plan which is really good. This should set things up for eventual "add more equations" phases of the project as well. I guess I could do this in Lean, and then we'll no longer need the Haskell finite_magma_tools."