proposition: Lemma eval_zero_inv: forall n m z, eval n m RegExp.zero z -> z=0.
proof: Proof. intros. dependent destruction H. auto. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(Reification)