Proof backends confuse uninterpreted constants with similar names

[brianhuffman]

If we define two constants with the same name (either by local definitions or by importing from more than one Cryptol module) the unint proof backends get confused and assume that they are the same constant.

For example, both of the prove_print commands in the following saw-script print "Valid":

let {{
  foo : [8] -> [8]
  foo x = 0
}};

let foo1 = {{ foo }};

let {{
  foo : [8] -> [8]
  foo x = x
}};

let foo2 = {{ foo }};

prove_print (unint_z3 ["foo"]) {{ \x -> foo1 x == foo2 x }};
prove_print (w4_unint_z3 ["foo"]) {{ \x -> foo1 x == foo2 x }};

Apparently both the sbv and what4 proof backends identify uninterpreted constants by their base names alone; we should additionally use unique ids to tell them apart. (Currently scConstant terms don't contain a unique id other than the one used for hash consing, which is actually optional. We should add a VarIndex to each scConstant like we do for ExtCns terms.)