proposition: Lemma compat_chain_dps : forall l a, chain_dps a l << succ_eq#.
proof: Proof. induction l; simpl; intros. apply compat_chain_dp. incl_trans (succ_eq# @ succ_eq#). comp. apply compat_chain_dp. apply IHl. apply comp_rtc_idem. Qed.
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)