I defined it in such way:

```
Definition eq_dec A := forall (x y: A), { x = y } + { x <> y }.
Definition index_error A (dec: eq_dec A) (x: A) (L: list A): option nat.
Proof.
induction L.
+ exact None.
+ destruct (dec x a).
- exact (Some 0).
- exact (match IHL with Some n => Some (S n) | None => None end).
Defined.
Definition index A (dec: eq_dec A) (default: nat) (x: A) (L: list A): nat :=
match (index_error dec x L) with
| Some n => n
| None => default
end.
```

Why do I think it would be nice to have? It is kind of inverse function of â€śnthâ€ť and seems useful for me anyway.

So, Iâ€™m collecting interesting/useful lemmas to prove about it. If you have any suggestions, feel free to post them.

Also, Iâ€™m trying to prove that

```
Theorem index_of_list_elements A (dec: eq_dec A) (d: nat) (L: list A) (H: NoDup L): map (fun i => index dec d i L) L = seq 0 (length L).
```

I know itâ€™s possible, because I have done it once already (but then the .v file become gibberish a day later - maybe electricity was lost in a bad moment or smth - and I hadnâ€™t saved it with version control software so it was lost and this time I have no success).

If anyone has any hints, I will be very grateful.