One of the most common problems for learners is avoiding assumptions that have no discharge strategy. The Make Assumption feature promotes good habits by requiring an explicit dischange strategy prior to making an assumption.

Deductions automatically renumbers lines and justifications when you insert or delete lines, or drag-and-drop from other proofs. And Deductions will even infer a formula from the justification in straightforward cases.