proposition: Theorem finite_pigeon_hole l m : length l < length m -> incl m l -> exists x aa bb cc, m = aa++x::bb++x::cc.
proof: Proof. intros; apply list_has_dup_eq_duplicates, finite_php_dup with l; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)