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).
Comments
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).