define simple_inst and fail to prove things about it

simple_inst renames type variables without any care about avoiding
accidental capture. I wanted to prove that this was equivalent to INST
on closed terms, but that's not true (see the example in the comment in
the file). It may be equivalent to INST on closed terms whose variables
all have distinct names; that might be the next thing to try...