proposition: Fact incl_cons_simpl x l m : l ⊆ m -> x::l ⊆ x::m.
proof: Proof. intros; apply incl_cons; simpl; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)