proposition: Lemma hd_red_Mod_of_chain : forall R : rules, chain R << hd_red_Mod (int_red R #) (dp R).
proof: Proof. intros. unfold chain, hd_red_Mod. refl. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil RelSub SN AShift ADPGraph VecUtil ASubstitution) Coq(List Lia)