work on proves_IMP, notice term translation is broken

it picks the wrong name for Tyrep and Tyabs tags (it should be the type
name).
fix term translation, and prove penultimate case of proves_IMP