proposition: Fact incl_cons_linv l m x : incl (x::m) l -> In x l /\ incl m l.
proof: Proof. intros H; split. + apply H; left; auto. + intros ? ?; apply H; right; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)