proposition: Lemma chain_chain_dp : forall t u, Chain t u -> exists a, chain_dp a t u.
proof: Proof. intros. do 2 destruct H. redtac. subst x. subst u. exists (mkRule l r). unfold chain_dp. simpl. intuition. exists s. intuition. Qed.
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)