Add check after each proof step, not just the end

In elaboration, unification errors aren't always fatal, because some
information may turn up later which fixes things. Interactive proofs
ought to have immediate feedback instead.
Fixes #974

It may also be worth considering automatically filling more things in by
unification (refine currently requires each explicit argument to be
given explicitly, because that is easier to explain). Possibly this
should be a different tactic.