proposition: Lemma dpg_unif_N_mark_correct : hd_rules_graph (red R' #) D' << Graph (dpg_unif_N R' D').
proof: Proof. apply dpg_unif_N_correct. hyp. rewrite forallb_forall. intros. unfold undefined_rhs. destruct (in_map_elim H). destruct H0. subst. destruct x0 as [l r]. simpl. unfold undefined. destruct r. rewrite forallb_forall in hypD. ded (hypD _ H). discr. simpl. rewrite negb_lr. apply undefined_hd_symb_dup_int_rules. Qed.
imports: Coq(Lia Compare_dec) CoLoR(ADecomp AUnif ARenCap ATrs ListUtil RelUtil AGraph LogicUtil AShift ACalls BoolUtil ADuplicateSymb ListDec EqUtil AHDE)