proposition: Fact perm_incl_right m l1 l2: l1 ~p l2 -> incl m l1 -> incl m l2.
proof: Proof. intros H1 H2 ? ?; apply Permutation_in with (1 := H1), H2; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)