repeatedly apply promote
Example and General Form:
Apply the promote command until there is no change. This command
``succeeds'' exactly when at least one call of promote ``succeeds''. In
that case, only a single new proof-builder state will be created.
Note: The split command is probably more helpful in many cases than