proposition: Fact lequiv_trans l m k : l ≃ₛ m -> m ≃ₛ k -> l ≃ₛ k.
proof: Proof. intros [] []; split; apply incl_tran with m; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)