Confluent relations

See merge request !53

The name made no sense and it was not used anywhere to my knowledge. If it
was used anywhere, it would be very unreliable as it contained hints like
`rtc_trans` that would generally lead to loops.

Seal `fresh_generic`.

See merge request !54

Since `fresh_generic` is too inefficient for all practical purposes, we seal
off its definition. That way, Coq will not accidentally unfold it during
unification or other tactics.

This issue actually occurred in iGPS, as reported by Hai.

silence fewer warnings, add comment about overwriting notation

See merge request !49

fix λ.. printing and test it

See merge request !51

Make trivial instances explicit

See merge request !50

This is in preparation for coq/coq#9274.

`tc_to_bool` to turn a type class into a Boolean that expresses if there is an instance

See merge request !48