fact: Fixpoint gerase n m (e: gregex n m): ugregex := match e with | g_zer _ _ _ => 0 | g_prd _ _ p => u_prd p | g_pls e f => gerase e + gerase f | g_dot e f => gerase e ⋅ gerase f | g_itr e => (gerase e)^+ | g_var i => u_var _ i end.
imports: kat gregex ugregex ordinal positives glang