Wip on the generalization using equations
Adding a test.

My current state of mind is as follows:

- in the best case, the inductive has a pattern structure, with
variables at the leaves. We proceed as before, building the diag.

- in the second to best case, the term has a pattern structure, with
non variable terms at the leaves and we are able to find a suitable
use of pattern that makes the abstracted term well typed: we introduce
this abstraction and the relevant equations, and we proceed to build
the diag with the pattern structure.

- in the last case, we forget about the pattern structure, if any, and
do as "dependent destruction" does, adding an explanatory warning that
states that we could not generalize this goal in a suitable manner.