Lean module conversion: implicit endpoints stop unifying

Converting a Lean 4 file to the module system (add module, public import, @[expose] public section after the module docstring) usually just works. In one file it broke: a definition's *type* was Edge.CompStruct (mapEdge F₁ h h') (mapEdge F₂ ..) (mapEdge F₃ ..), where mapEdge {x y} got its endpoints from unification with the CompStruct binders. As a module, one by simpa ... using h argument ran before that unification and failed with 'tactic execution is stuck, goal contains metavariables'. The fix is to pass the implicit endpoints explicitly (mapEdge (x := x₀) (y := x₂) ...). A non-module file cannot be imported by a module file ('cannot import non-module'), so convert bottom-up along the import graph and build after each file. It took ~10 min for 6 files.