proposition: Lemma lequiv_lseq l m : l ≃ₛ m -> l ≡ m.
proof: Proof. intros H; apply lequiv_lc in H as (c & []); eauto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)