Add class `HasLcIf`

This makes it easier to write generic adequacy lemmas, you don't have to write the rather ugly if use_credits ... but can use the HasLcIf class. This is not only useful for Iris, but also downstream. Developments like Iron have their own adequacy results and ideally we have a generic version there.

The classes HasLc and HasNoLc are now notations.

This also makes TC inference a bit better, we got rid of some uses of first done, which are now automatically inferred by TC.