proposition: Lemma chain_hd_red_mod : chain << hd_red_mod R dp.
proof: Proof. unfold chain, hd_red_mod. comp. apply rtc_incl. apply int_red_incl_red. Qed.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)