ESPL: Change IH for well-typedness proofs

Cases with a non-trivial type on the LHS of a match step could not be
proven automatically before. This essentially reverts commit
baf957f9661e90cbd947e85688e41ec799a32348. The old IH works now
because of the improvements by bb6a08084103eae81e04743af3ba4606458167a0.
Improve type inference