proposition: Lemma dpg_unif_N_correct : hd_rules_graph (red R #) D << Graph dpg_unif_N.
proof: Proof. incl_trans dpg_unif. apply dpg_unif_correct. intros r1 r2 h. destruct h. destruct H0. unfold Graph, dpg_unif_N. rewrite <- mem_ok in H. rewrite <- mem_ok in H0. rewrite H, H0. bool. destruct (iter_step_complete (wf_mk_problem (ren_cap r1 r2) (lhs r2)) H1). unfold connectable_N, unifiable_N. case (lt_eq_lt_dec x N); intro. destruct s. ded (successfull_preserved H2 l). destruct (successfull_elim H3). rewrite H4. refl. subst. destruct (successfull_elim H2). rewrite H3. refl. ded (successfull_inv H2 l). destruct (iter_step N (mk_problem (ren_cap r1 r2) (lhs r2))). 2: cong. destruct p. destruct e. refl. eapply successfull_hd_eq. rewrite <- mem_ok. hyp. rewrite <- mem_ok. hyp. apply H2. Qed.
imports: Coq(Lia Compare_dec) CoLoR(ADecomp AUnif ARenCap ATrs ListUtil RelUtil AGraph LogicUtil AShift ACalls BoolUtil ADuplicateSymb ListDec EqUtil AHDE)