proposition: Lemma commute_build_empty: forall e, Algebraic.build e 0 1 Algebraic.empty [=0=] preNFA_to_preMAUT (build e 0 1 empty).
proof: Proof. intros. rewrite <- commute_build, <- commute_empty. reflexivity. apply bounded_empty. reflexivity. reflexivity. 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_CheckLabels) ATBR(StrictStarForm) ATBR(Utils_WF) Coq(Relations)