Adding hypotheses

[tlringer]

When can this be done usefully? What do useful equivalences for this look like? Consider the ornamental promotion isomorphism when the inductive type doesn't change structure. Evolve from that to new inductive structure. What is the most useful way to get the "patch"? And so on. Develop a few manual examples, build search procedures later if wanted.