Hitting Ctrl+J adds a conclusion to the proof. A conlusion is always added after the current line, or, if the line is a premise, then the conclusion is added after the last premise. If the current line is a conclusion, then it is highlighted in cyan.
Hitting Ctrl+P adds a premise to the proof. A premise will always be added after the last premise.
Pressing Ctrl+B adds a subproof to the proof. When in a subproof, a conclusion will always be added within the subproof. The first line of a subproof does not require a rule, but instead acts as a premise. Pressing Ctrl+D ends the current subproof. This creates a new conclusion just after the subproof.
To undo a command, simply press Ctrl+Z. This will undo the last text modification, insertion, or deletion. In the case of several insertions or several deletions, undo will undo all of them. To undo an undo, press Ctrl+Y, or redo.