To find the purpose of the rewrite, try removing it and seeing what happens!

Also, two comments:

1. Why do you write the minus in prefix position? I did that with plus and
times to match on their implicit arguments, but you don't need that here.

2. Why this particular type signature? Is there a use case in mind? The one
for addition is for indexing into a Vect that results from appending two
Vects, while the multiplication is for indexing into a Vect of Vects. Other
possibilities for Fin subtraction include statically checking that the
second arg is bounded by the first, reducing the bound by the second arg,
and probably a few more.