proposition: Lemma compat_chain_dp : forall a, chain_dp a << succ_eq#.
proof: Proof. intros. incl_trans (red_mod R DP). apply incl_trans with Chain; try incl_refl. apply chain_dp_chain. incl_trans (hd_red_mod R DP). apply chain_hd_red_mod. apply hd_red_mod_incl_red_mod. incl_trans (succ_eq!). apply compat_red_mod_tc; hyp. apply tc_incl_rtc. Qed.
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)