work on proves_IMP constant cases

and add a missing condition to the inference system: abs and rep
constant names must be distinct.