proposition: Fact lseq_lequiv l m : l ≡ m -> l ≃ₛ m.
proof: Proof. induction 1 as [ | ? ? ? ? [] | | | ? ? ? [] | ? ? ? ? [] ? [] ]; eauto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)