proposition: Lemma lequiv_lc l m : l ≃ₛ m -> exists c, l ⪼ c /\ m ⪼ c.
proof: Proof. induction on l m as IH with measure (⌊l⌋+⌊m⌋); intros H1. destruct (lequiv_php_choose H1) as [ H2 | [ H2 | H2 ] ]; eauto. + apply lhd_lc in H2 as (c & ? & ?). destruct (IH c m) as (d & ? & ?); eauto; lia. + apply lhd_lc in H2 as (c & ? & ?). destruct (IH l c) as (d & ? & ?); eauto; lia. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)