finish proof of semantics_simple_inst

needed extra assumptions that the variable names in the term are all
distinct (which is not surprising, if simple_inst is going to work...)