I agree, but what would be more useful is instead of copy-pasting the same thing everywhere, you write it once and you can reuse it like a function. This will require it to be able to be extracted as a separate tree and then be referenced when needed.
30 days ago(+1)
Do you mean essentially like a custom "rule" (lemma) which you could then use like an ordinary rule wherever it fits? So basically a kind of template instead of a plain copy.
Yeah, could be thought of like that. A template being a custom combination of rules that you can use like a normal rule.
Here i use P from P^Q and then Q from P^Q, but instead of using this twice, i would make a template with both rules and it will then say Q from (P^Q)^R. It could be a big technical hurdle to make it work correctly though, or it may end up being easy using the already existing way to create trees from rules, just replacing A, B, C with P, Q, R.
And now that i think about it, functions/templates could be very useful if made persistent.
For example i want to more easily say that things are commutative. I create a new template Q^P from P^Q. Now i can reuse this custom template everywhere like a rule.
28 days ago(+2)
A simple solution for persintence could be that every level (at least the named ones), after solved, becomes a new rule you can use. Need some way of organizing so you can easily find them, though. If/when I add first order logic I think something like this would be very useful or the proofs might get very long.