fact: Fixpoint re_opt_e {T:Type} (re: reg_exp T) : reg_exp T := match re with | App EmptyStr re2 => re_opt_e re2 | App re1 re2 => App (re_opt_e re1) (re_opt_e re2) | Union re1 re2 => Union (re_opt_e re1) (re_opt_e re2) | Star re => Star (re_opt_e re) | _ => re end.
imports: Coq(Arith List) LF(IndProp)