type rewriting

Stream: new members

[Antoine Chambert-Loir]

At some point of a proof, I have terms x : fin m and h : m = n, and I need to produce y : fin n.
However, the naturalrw h at x produces a new x : fin n which I can't relate to the earlier one (which my goal proof indicates as x_1).
What can I do?

[Reid Barton]

Use docs#fin.cast