(*#* We prove that there is only one proof of [x=x], i.e [(refl_equal ? x)].
This holds if the equality upon the set of [x] is decidable.
(*#* We prove that there is only one proof of [x=x], i.e [(refl_equal ? x)].
This holds if the equality upon the set of [x] is decidable.