We have assumed everywhere that unification is done automatically in the background. Unification instantiates forall-quantified variables, thereby doing scope applications (function applications). Side condition of those applications is that the function argument is in the function's domain. Thus we have to prove this condition for every instantiation done. I'll call such an addition proof-goal a "debt".
Here's what the user should be able to do with his debt:
- eyeball-check that a statement is provable before pushing it into debt
- at every point be able to choose between continue proving along the main thread or working off some debt
- keep track of all the context that belongs to every item of debt
- be able to find and apply proof steps that have preconditions, e.g. for "a ⇒ x=y": replace x by z and make a debt