proposition: Lemma chain_dps_app : forall l a b m, chain_dps a (l ++ b :: m) << chain_dps a l @ chain_dps b m.
proof: Proof. induction l; simpl; intros. refl. assoc. comp. apply IHl. Qed.
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)