Make names more consistent with the rest of the development, make
definitions type classes opaque so that the proofmode does not unfold
then, declare timeless, persistent and proper instances.