[Agda] subst puzzle

[Paolo Capriotti]

March 1, 2021 9:54 pm:
> Here is a self-contained puzzle that has me stumped. I'm sure there are 
> lemmas in Relation.Binary.PropositionalEquality.Properties that ought to 
> apply, but I just can't see it.  Ideas?

Here is my attempt:
https://gist.github.com/pcapriotti/32358d5b89e72459608651e6030886de

I find the easiest way to prove an equality of elements of Fin n is to just convert them to natural numbers, prove the equality there, then using injectivity of toℕ.

Best,
Paolo