LuiUnification

When an interactive unification attempt fails, LUI can display the partial result with failure sites highlighted and detailed. The user can navigate between the (potentially numerous) unification failures using the left and right arrow keys.