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: Jul 25 2024 at 16:02 UTC