proposition: Lemma dup_seq (f : nat -> X) start len : not (NoDup (map f (seq start len))) -> exists '(i, j), f i = f j /\ (start <= i /\ i < j /\ j < start+len).
proof: Proof. Proof using X_eq_dec. move=> /not_NoDupE [[i j]]. rewrite map_length seq_length. move=> [? H]. exists (start+i, start+j). split; last lia. move: H. rewrite ?nth_error_map ?nth_error_seq; [lia|lia|]. by move=> []. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun