[Agda] subst puzzle

[James Chapman]

Here's a slight variation - replacing Paolo's nice observation about
moving from Fin to Nat with some more mindless subst management:

https://gist.github.com/jmchapman/190acbc1c2b8f5d3fb5224a7f46d1bb5

Regards,

James

On Tue, 2 Mar 2021 at 07:39, Paolo Capriotti <paolo at capriotti.io> wrote:
>
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda