Add special support for forgetful functors

[SReichelt]

If a definition or theorem is written for e.g. semirings, it cannot easily be applied to e.g. a ring. This is because the ring cannot transparently be regarded as a semiring, even though that seems trivial.

It is not possible to use (an extended version of) embeddings for this purpose because the corresponding functions are not injective. Instead, this should probably work similarly to type coercion in other systems.

This is somewhat related to the "explicit structures" part of #46, as there needs to be a simple way to specialize e.g. a theorem about semirings to e.g. the ring of integers.

Possibly, definitions of finite, infinite, and more general sequences can be consolidated using this feature.