Prior to this change there was a bit of a mess in handling of types on
which you can do `CAS` and which you can compare by equality.
This change adds typing rules that allow `CAS` on any unboxed types.

Due to changes to Coq's import mechanism, I now made sure that
Autusubst is imported first. This caused various things to break,
which I patched up.

Lty2 → LRel (logical relation)
proofmode.v → reloc.v

This simplifies the value interpretations a lot.

There is now a separate `REL e1 << e2 @ E : A` proposition,
on top of which we define the semantic typing judgement.

All the tactics work on the `REL .. << ..` proposition, and we use it
to prove the fundamental property. This means that we have to deal
with substitutions whenever we are doing something with the typing
judgement, but in practice this is not so bad.

Also added and updated: the counters refinement example.

+ better notation thanks to robbert