proposition: Fact incl_cons_r_inv x l m : m ⊆ x::l -> exists m1 m2, m ~p m1 ++ m2 /\ Forall (eq x) m1 /\ m2 ⊆ l.
proof: Proof. intros H. apply (@incl_app_r_inv (x::nil) _ l) in H as (m1 & m2 & H1 & H2 & H3). exists m1, m2; msplit 2; auto. rewrite Forall_forall. intros a Ha; apply H2 in Ha; destruct Ha as [ | [] ]; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)