[WIP] Add proof step verification.

[Kripner]

Verify each proof step in tactic mode. Roughly, the idea for step (old :: ProofSnapshot, new :: ProofSnapshot) is to:

• (1) Look at all goals in old which no longer exist in new. For each one:
  • (2) Retrieve it's assignment in new. For each metavariable in the assignment:
    • (3) If it is a goal which exists in new, it's fine and we do nothing since we can assume it will be solved in future steps. In this case, we replace it with sorry in the assignment so that the expression can be sent to kernel.
    • (4) Otherwise, it's an error since there is a metavariable which won't be assigned in the future.
  • (5) Send the assignment with metavariables replaced by sorry to kernel for a type check.

Compared to #63, this approach could eliminate false negatives like https://github.com/leanprover-community/repl/blob/master/test/name_generator.in, where checking the whole proof term doesn't work since in a have branch we don't see the metavariable assignments from the main branch.