comparison: treat prophecies like unit and make all closures equal

As @amintimany noted, currently erasure actually does not hold (so much for obvious^^) because the program could compare two prophecy variables to figure out if they are equal -- so after replacing them all by unit, the result changes.

To fix this, we make comparison use a "normalization" function to replace all prophecies by unit before comparing. Amongst the options I considered, I think this is the least intrusive. The alternative is to get stuck if either of the compared values contains a prophecy, but that does not usually compute away as nicely as this normalization function.

While at it, this "normalization" function is also used to fix the problem that in heap_lang you can compare closures: normalization replaces all closures by a fixed one (fun _ => ()), this making all closures the same but distinct from anything else.