Open emiquey opened 2 years ago
When you realize that you should have first exchanged then use the ⊗-intro rule, you have to remove the rule/exchange/⊗-intro again.
Short answer to this (when there is only one ⊗-intro rule above): actually it is not the case, since you can just exchange the formulas then click on the appropriate tensor and it does the job.
For situations with a tentative modification deeper in the proof, you may face additional difficulties:
A nice feature that could be added would be to be able to exchange formulas below a ⊗-intro rule and to have the premises updated. For instane, consider the following bad attempt . When you realize that you should have first exchanged then use the ⊗-intro rule, you have to remove the rule/exchange/⊗-intro again. I don't if it makes sens in any other situation (that is, lower in a tree), and if it would be hard to add, but if it is not too much work I think it's worth it !