proposition: Fact incl_cons_l_inv l m x : x::m ⊆ l -> x ∈ l /\ m ⊆ l.
proof: Proof. intros H; split. + apply H; simpl; auto. + apply incl_tran with (2 := H); simpl; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)