proposition: Lemma complete_compat_left : forall {tar} `{DS.WF tar} {tar'} `{DS.WF tar'} l, tar [=T=] tar' -> tar +++l [=T=] tar' +++ l.
proof: Proof. intros ? ? ? ? ? H. split; apply complete_incr_left; apply H. 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)