proposition: Theorem finite_php_dup l m : length l < length m -> incl m l -> list_has_dup m.
proof: Proof. intros H1 H2. destruct (@length_le_and_incl_implies_dup_or_perm l m) as [ | H3 ]; auto; try lia. apply Permutation_length in H3; lia. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)