proposition: Lemma pigeonhole {X : Type} (L L' : list X) : incl L L' -> length L' < length L -> not (NoDup L).
proof: Proof. move=> ?? HL. suff: length L = length L' by lia. apply /Permutation_length /NoDup_Permutation_bis; by [|lia]. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun