Prompt for ambiguous cases instead of failing

[joom]

Currently if a rule is applicable to multiple formulas in a sequent, the applyLK function fails. It should instead ask the user which one they mean.

However, this cannot be done with JavaScript's built-in prompt (unless you ask the user which one they mean, requiring them to enter a number which would be the order. but that's ugly). So it needs to create a modal window, which should also fit well with the general design of the app.