proposition: Fact lequiv_app_comm l m : l++m ≃ₛ m++l.
proof: Proof. split; intros ?; rewrite !in_app_iff; tauto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)