forall n L, length L = n -> map (fun i => nth i L 0) (seq 0 n) = L

but how to do induction to prove it?

Induction by L or by n doesnâ€™t work (for me). Induction by n feels the closest to the correct solution because of (seq 0 n). Should I somehow generalize the statement?

I would use the following (easy to prove) two lemmas:

Lemma list_eq_nth (X : Type) (def : X) (xs ys : list X) :
(forall n, n < length xs -> nth n xs def = nth n ys def) ->
length xs = length ys ->
xs = ys.
Lemma map_nth' (A B : Type) (f : A -> B) (l : list A) (d1 : B) (d2 : A) (n : nat) :
n < length l ->
nth n (map f l) d1 = f (nth n l d2).

This one is a natural strengthening of nth_ext (in List in master). I have a running pull request on some statements of List, I will try to incorporate this modification (with two default values def and def').

This one is mostly map_nth with nth_indep for d1 <> f d2.

I like Olivierâ€™s suggestion of doing reverse induction on L. I left the SearchAbout commands I used to find the names of the right lemmas in the library in the script, because they might be instructive:

Require Import List Permutation Omega.
Set Implicit Arguments.
Theorem thm01 (L: list nat): map (fun i => nth i L 0) (seq 0 (length L)) = L.
Proof.
induction L using rev_ind.
- reflexivity.
- rewrite app_length, seq_app, map_app.
Search app nth length.
cbn. rewrite app_nth2, Nat.sub_diag.
+ rewrite <- IHL at 2.
f_equal.
Search map "ext".
apply map_ext_in.
intros n [_ H] % in_seq.
now apply app_nth1.
+ omega.
Qed.