proposition: Fact incl_cons_rinv x l m : incl m (x::l) -> exists m1 m2, m ~p m1 ++ m2 /\ Forall (eq x) m1 /\ incl m2 l.
proof: Proof. intros H. apply (@incl_app_rinv (x::nil) _ l) in H. destruct H as (m1 & m2 & H1 & H2 & H3). exists m1, m2; repeat split; auto. rewrite Forall_forall. intros a Ha; apply H2 in Ha; destruct Ha as [ | [] ]; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)