proposition: Lemma hd_red_Mod2_hd_rules_graph : forall t u v, hd_red_Mod S D t u -> hd_red_Mod S D u v -> exists a1, exists a2, hd_rules_graph a1 a2.
proof: Proof. intros. ded (hd_red_Mod_chain_hd_rules H). ded (hd_red_Mod_chain_hd_rules H0). destruct H1. destruct H2. exists x. exists x0. eapply hd_red_Mod_rule2_hd_rules_graph. apply H1. apply H2. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil RelSub SN AShift ADPGraph VecUtil ASubstitution) Coq(List Lia)