fact: Fixpoint collect e acc := match e with | RegExp.var i => NumSet.add i acc | RegExp.plus a b => collect a (collect b acc) | RegExp.dot a b => collect a (collect b acc) | RegExp.star a => collect a acc | _ => acc end.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(DKA_Definitions) ATBR(StrictStarForm)