proposition: Lemma chain_hd_rules_hd_red_Mod : forall a, hd_red_Mod_rule a << hd_red_Mod S D.
proof: Proof. unfold inclusion. intros. destruct H. do 2 destruct H0. exists (sub x0 (lhs a)). split;auto. subst y. destruct a. simpl in *. unfold hd_red. exists lhs; exists rhs; exists x0. auto. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil RelSub SN AShift ADPGraph VecUtil ASubstitution) Coq(List Lia)