proposition: Lemma hd_rules_graph_incl : forall S D D', incl D D' -> hd_rules_graph S D << hd_rules_graph S D'.
proof: Proof. intros. intros a b h. destruct h. decomp H1. unfold hd_rules_graph. intuition. exists x. exists x0. hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil RelSub SN AShift ADPGraph VecUtil ASubstitution) Coq(List Lia)