proposition: Lemma NoDup_alt l : NoDup l ↔ ∀ i j x, l !! i = Some x → l !! j = Some x → i = j.
proof: Proof. split; eauto using NoDup_lookup. induction l as [|x l IH]; intros Hl; constructor. - rewrite elem_of_list_lookup. intros [i ?]. opose proof* (Hl (S i) 0); by auto. - apply IH. intros i j x' ??. by apply (inj S), (Hl (S i) (S j) x'). Qed.
imports: stdpp(options)