+ * generation of derived lemmas rewritten to be based on hooks that
+ are triggered every definition
+ * composition of coercions fixed, more composite are generated
+ * undo mechanism for coercions remade, should work better
+ * new command "prefer coercion foo" to reorder coercions.