Every list element has an index

Stream: new members

[Martin Dvořák]

I need the following observation or some variation on it. Any idea, please?

example (lis : list char) (c : char) (h : c ∈ lis) :
  ∃ n : ℕ, ∃ n_lt_len : (n < lis.length), c = (list.nth_le lis n n_lt_len) :=
begin
  sorry,
end

[Jireh Loreaux]

docs#list.mem_iff_nth_le