Hello!

Any hints how to prove this? Thanks in advance.

```
Require Import List Permutation.
Theorem thm n (L1 L2: list nat) (H1: Permutation L1 (seq 0 n)) (H2: Permutation L2 (seq 0 n)):
NoDup (map (fun i => nth i L1 0) L2).
```

This is the missing part of attempt to prove

```
Theorem perm_mult_thm n (L1 L2: list nat) (H1: Permutation L1 (seq 0 n)) (H2: Permutation L2 (seq 0 n)):
Permutation (map (fun i => nth i L1 0) L2) (seq 0 n).
```