Tracking list of feature requests:

• A proof is a tree.  In a tree, a goal is associated with each node.  Each node is annotated with a integer sequence (starting with the marker "top" which corresponds to the statement to prove) that depends on the node's location in the tree.  For example, the first subgoal of the second subgoal of the proof of a lemma is annotated with the sequences "top 2 1".  It could be useful instead to display, e.g., "top 2/3 1/2" if the top node had 3 subgoals and the second subgoal had itself 2 subgoals.