fact: Fixpoint vars (e: regex') := match e with | r_zer | r_one => nil | r_pls e f | r_dot e f => app (vars e) (vars f) | r_str e => vars e | r_var a => cons a nil end.
imports: syntax kleene boolean lang lset sums normalisation