proposition: Lemma eval_one_inv: forall n m c, eval n m RegExp.one c -> c [=] one (typ n) /\ n=m.
proof: Proof. intros. dependent destruction H. split; reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(Reification)