proposition: Lemma add_lists_sameclass: forall {tar} `{DS.WF tar} ml a x y l, a < ml -> {{tar +++ add_lists x y ml l}} (delta a x) (delta a y).
proof: Proof. intros tar Hwf ml; revert tar Hwf. induction ml; intros. lia_false. simpl. destruct (eq_nat_dec a ml). subst. apply complete_incr. apply in_union. apply IHml; ti_auto. lia. 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)