proposition: Lemma not_NoDup_consE {x} {l: list X} : (not (NoDup (x :: l))) -> In x l \/ not (NoDup l).
proof: Proof. Proof using X_eq_dec. have [?|?] := In_dec X_eq_dec x l. { move=> ?. by left. } move=> Hxl. right => Hl. apply: Hxl. by constructor. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun