proposition: Lemma chain_dps_path_dp_graph : forall l a b t u, chain_dps a (l ++ b :: nil) t u -> path dp_graph a b l.
proof: Proof. induction l; simpl; intros; do 2 destruct H. eapply chain_dp2_dp_graph. apply H. apply H0. ded (IHl _ _ _ _ H0). intuition. destruct l; simpl in H0; do 2 destruct H0. eapply chain_dp2_dp_graph. apply H. apply H0. eapply chain_dp2_dp_graph. apply H. apply H0. Qed.
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)