proposition: Lemma chain_dps_app' : forall a l m b p, a :: l = m ++ b :: p -> chain_dps a l << chain_dps a (tail m) % @ chain_dps b p.
proof: Proof. intros. destruct m; simpl in H; injection H; unfold inclusion; intros. subst p. subst b. exists x. unfold clos_refl. intuition. subst r. subst l. simpl. ded (chain_dps_app _ _ H2). do 2 destruct H0. exists x0. unfold clos_refl. intuition. Qed.
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)