proposition: Fact incl_app_r_inv l m p : m ⊆ l++p -> exists m1 m2, m ~p m1++m2 /\ m1 ⊆ l /\ m2 ⊆ p.
proof: Proof. induction m as [ | x m IHm ]. + exists nil, nil; auto. + intros H; apply incl_cons_l_inv in H as (H1 & H2). destruct (IHm H2) as (m1 & m2 & H3 & H4 & H5). apply in_app_or in H1 as []. * exists (x::m1), m2; simpl; auto. * exists m1, (x::m2); simpl; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)