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