Make note of unapplied unifiation solutions

i.e. when an argument is given explicitly, but can be solved by
unification, make sure that the given argument and the inferred argument
themselves unify. Keep track in the ProofState structure, and unify when
'solve' tactic is applied for the given hole.

Fixes #765