proposition: Fact incl_swap (x y : X) l : x::y::l ⊆ y::x::l.
proof: Proof. intros ? [ -> | [ -> | ] ]; simpl; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)