proofs are sequent proofs organized in a refinement style. In other words they are trees where each node contains a goal and a rule application. The children of a node are the subgoals of their parent; in order to prove the parent it is sufficient to prove the children. ( automatically generates the children, given their parent and the rule to be applied; it is never necessary to type them in.) Not all goals have subgoals; for example, a goal proved by hyp does not. Also, an incomplete goal (one whose rule is bad or missing) has no subgoals.
In what follows the main goal ( the goal for short) is the goal of the current node; a goal is either the main goal or one of its subgoals.