Draft: Represent values only with their abstract version

[clarus]

This branch represent some work and I am not sure it is that useful. This idea is to add a type A.t:

Module A.
  Inductive t : Set :=
  | Make {A : Set} (x : A) (to_value : A -> Value.t).
End A.

that forces to keep the values abstract. But it also complexifies the semantics rules.