proposition: Lemma not_NoDupE {l : list X} : not (NoDup l) -> exists '(i, j), i < j < length l /\ nth_error l i = nth_error l j.
proof: Proof. Proof using X_eq_dec. elim: l. { move=> H. exfalso. apply: H. by constructor. } move=> x l IH. move=> /not_NoDup_consE [|]. - move=> /(@In_nth_error X) [j] Hj. have ? : not (length l <= j). { move=> /nth_error_None. by rewrite Hj. } exists (0, S j) => /=. split; [lia|done]. - move=> /IH [[i j]] [? ?]. exists (S i, S j) => /=. split; [lia|done]. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun