I proved something like what follows, but what is the best way to avoid using `deprecated_filter_index_enum`

?

```
Lemma foo (k : 'I_10) : k \in enum 'I_10.
Proof. by rewrite -deprecated_filter_index_enum map_f. Qed.
```

anything wrong with:

```
Proof. by rewrite mem_enum. Qed.
```

Thanks. I didn't think about this intermediate rewriting step.

Pierre Jouvelot has marked this topic as resolved.

Last updated: Jul 25 2024 at 15:02 UTC