Prevent the same formula/term/conclusion from being formed more than once

[Voileexperiments]

Currently these things will not produce duplicates when being created:

• free/bound variables created by New free/bound variable
• environments (if a conclusion belongs to an environment that already exists, it will go into the existing one)

However, these things will produce duplicates:

• formulas
• terms constructed by predicates/operator window
• conclusions (moreover, doing the same conclusion will incur another step lost)

Ideally, each of the above should not have duplicates. Doing the same conclusion should be a no-op, and arguably doing a step that reaches a conclusion that already exists should also be a no-op?

[teorth]

This should now be implemented (in the sense that duplicate boxes are not created, but the step is still made).