proposition: Lemma iter_chain_chain_dps : forall n t u, iter Chain n t u -> exists a, exists l, length l = n /\ chain_dps a l t u.
proof: Proof. induction n; simpl; intros. ded (chain_chain_dp H). destruct H0. exists x. exists nil. intuition. do 2 destruct H. ded (chain_chain_dp H). destruct H1. exists x0. ded (IHn _ _ H0). do 3 destruct H2. exists (x1 :: x2). simpl. intuition. exists x. intuition. Qed.
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)