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.