Re: [Haskell-cafe] GADTs: the plot thickens?

Bruno,

Now we modify thin to take an extra Nat n (not needed, but just to show the duality with thickening):

I'm puzzled by the "not needed" bit. Isn't the introduction of Fin's indices reflected as values in the GADT , and the fact that the GADT makes that reflection, what makes it work? P.