proposition: Lemma dpg_unif_correct : hd_rules_graph (red R #) D << dpg_unif.
proof: Proof. intros x y h. destruct h. decomp H0. unfold dpg_unif. intuition. destruct x as [l1 r1]. destruct y as [l2 r2]. simpl in *. unfold connectable. set (k := S (maxvar l2)). destruct (rtc_red_sub_ren_cap hypR k H2). destruct (ren_cap_sub R x1 r1 k). destruct H3. revert H0. rewrite H3. unfold shift. rewrite !sub_sub. intro. assert (forall x, In x (vars (ren_cap R k r1)) -> In x (vars l2) -> False). intros. ded (vars_ren_cap H5). ded (vars_max H6). subst k. lia. unfold unifiable. eapply sub_eq_is_sol. hyp. symmetry in H0. apply H0. Qed.
imports: Coq(Lia Compare_dec) CoLoR(ADecomp AUnif ARenCap ATrs ListUtil RelUtil AGraph LogicUtil AShift ACalls BoolUtil ADuplicateSymb ListDec EqUtil AHDE)