proposition: Lemma chain_dp_chain : forall a, chain_dp a << Chain.
proof: Proof. unfold inclusion. intros. destruct H. do 2 destruct H0. exists (sub x0 (lhs a)). intuition. subst y. destruct a. simpl. apply hd_red_rule. exact H. Qed.
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)