proposition: Fact lc_lequiv l m : l ⪼ m -> l ≃ₛ m.
proof: Proof. intro; apply lseq_lequiv; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)