proposition: Fact perm_incl_left m1 m2 l: m1 ~p m2 -> incl m2 l -> incl m1 l.
proof: Proof. intros H1 H2 ? H. apply H2; revert H; apply Permutation_in; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)