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