proposition: Lemma restricted_dp_graph : is_restricted hd_rules_graph D.
proof: Proof. unfold is_restricted, hd_rules_graph, inclusion. intros. intuition. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil RelSub SN AShift ADPGraph VecUtil ASubstitution) Coq(List Lia)