fact: Fixpoint contains_one e : bool := match e with | RegExp.star a => true | RegExp.one => true | RegExp.plus a b => contains_one a ||| contains_one b | RegExp.dot a b => contains_one a &&& contains_one b | _ => false end.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(Monoid) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(Model_RegExp) Coq(Bool)