proposition: Theorem lequiv_ind l m : l ≃ₛ m -> P l m.
proof: Proof. Proof using All. rewrite <- lseq_lequiv_iff; induction 1; eauto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)