proposition: Lemma diag_compat_left : forall {tar} `{DS.WF tar} {tar'} `{DS.WF tar'}, tar [=T=] tar' -> forall l, diag {{tar}} {{tar +++ l}} -> diag {{tar' }} {{tar'+++l}}.
proof: Proof. intros tar Hwf tar' Hwf' Heq l H a x y Hx Hy Ha Htar. rewrite <- Heq in Htar. specialize (H a x y Hx Hy Ha Htar). refine (complete_incr_left _ H). apply Heq. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(DKA_StateSetSets) ATBR(Utils_WF) Coq(Relations) Coq(List)