Improve `suffices by`

[tsani]

It would be great if one could write suffices by i by itself and interactively fill in the concrete types of the arguments. That is, the interaction would look something like:

Meta-context: ...
Computational context: ...
-----------------------------
Goal: whatever
> suffices by i
1. tau_1: tau_1'
2. tau_2: tau_2'
...
n. tau_n: tau_n'

where T_1, T_2, ..., T_n are obtained from the type synthesized by i. That is, we require that i synthesize a type of the form Pi X_1 : U_1. ... Pi X_m : U_m. tau_1 -> ... -> tau_n.

This new suffices by i should immediately find the conclusion of the type of i and unify it with the goal type to check that i is at least compatible with the current goal. Then, the user specifies the specialized types of the inputs tau_1', tau_2', ..., tau_n' which are unified with the types of the abstract input types in order to pin down instantiations for all the universally quantified variables. It would be great if this unification can be done "as we go" so that if the user incorrectly types a premise type, they can immediately correct it. Leaving a premise type empty should abort this loop. Once all premise types have been established, the suffices command proceeds as usual.