proposition: Lemma chain_dps_iter_chain : forall l a, chain_dps a l << iter Chain (length l).
proof: Proof. induction l; simpl; intros. apply chain_dp_chain. comp. apply chain_dp_chain. apply IHl. Qed.
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)