fact: Fixpoint epsilon (e: regex') := match e with | r_one | r_str _ => true | r_pls e f => epsilon e || epsilon f | r_dot e f => epsilon e && epsilon f | _ => false end%bool.
imports: syntax kleene boolean lang lset sums normalisation