proposition: Lemma add_lists_S: forall {tar} `{DS.WF tar} x y a l, {{tar}} (delta a x) (delta a y) -> tar+++add_lists x y (Datatypes.S a) l [=T=] tar+++add_lists x y a l.
proof: Proof. intros tarjan Hwf x y a l H. simpl complete at 1. apply complete_compat_left. split; intros u v Huv. rewrite DS.sameclass_union in Huv. num_simpl. destruct Huv as [Huv | [[Hu Hv]|[Hu Hv]]]; auto. rewrite Hu, Hv; assumption. rewrite Hu, Hv; symmetry; assumption. apply DSUtils.le_union, Huv. 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)