[siraben]

Thank you for the feedback! Will address. Yeah, I intentionally tried to not make the UI too easy to prove things and it shows all possible actions that can be taken from the current point, so that in the future another mode could be added for writing proofs from scratch.

[amavect]

Just thought of how to fix the problem I had. Since the program already highlights the inductive hypothesis blue (but doesn't underline), consider adding a clickable underline to it (Rewrite with IH) instead of requiring the green IH box on the left (banner blindness). See if you can get rid of any drag&drop features and focus more on underline and click (TouchProof, not DragProof). Then the tip box would only need to explain clicking underlined terms.

And another thing, when 2 underlined terms nest (say, Sn+0=0 with underlines on Sn+0 and n), hovering should highlight only the more specific term (hovering on n highlights both Sn+0 and n the same color).