proposition: Lemma lequiv_lhd_or_contract l m : l ≃ₛ m -> lhd m \/ l ⪼ m.
proof: Proof. simpl; intros H. destruct lequiv_lc with (1 := H) as (d & H1 & H2). apply lc_length_perm in H2 as [ H2 | H2 ]. + apply finite_php_dup in H2; auto. apply lc_lseq, lseq_lequiv in H1. apply incl_tran with l; tauto. + right; apply lc_trans with (1 := H1). apply perm_lc, Permutation_sym; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)