proposition: Lemma lequiv_php_choose l m : l ≃ₛ m -> l ~p m \/ lhd l \/ lhd m.
proof: Proof. intros [ I1 I2 ]. destruct (le_lt_dec ⌊m⌋ ⌊l⌋) as [ H1 | H1 ]. + apply length_le_and_incl_implies_dup_or_perm in H1; tauto. + apply finite_php_dup in H1; tauto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)