Assuming I have some `T : eqType`

together with a proof of `Finite.axiom Ts`

for some `Ts : seq T`

. Is there a direct way of turning `T`

into a finite type, that does not involve explicitly mentioning any `pickle`

/`unpickle`

function to get the required `countType`

instance?

I think that's a missing piece indeed...

Okay, in my case, `Ts`

is actually a concrete nonempty list enumerating an inductive without parameters , so I can do:

```
Lemma foo: cancel (index^~ Ts) (nth t0 Ts). Proof. by case. Qed.
```

followed by the usual litany of instances for `countType`

, `choiceType`

, and `finType`

. Oh well...

Last updated: Jan 29 2023 at 19:02 UTC