better transitivity properties.

The only remaining non-linear file is non-linear on purpose

Decidability is replacedby a non-confluent non-linear rewrite-system

It should not have been tracked in the first place.

a digit.

Still rely on String_UIP.

definition of types

Even for Assoc, which is a bit heavy but works well.

coerce is now a smart constructor.

Examples pass.