proposition: Lemma NoDup_lookup l i j x : NoDup l → l !! i = Some x → l !! j = Some x → i = j.
proof: Proof. intros Hl. revert i j. induction Hl as [|x' l Hx Hl IH]. { intros; simplify_eq. } intros [|i] [|j] ??; simplify_eq/=; eauto with f_equal; exfalso; eauto using elem_of_list_lookup_2. Qed.
imports: stdpp(options)