proposition: Lemma uglang_gerase n m (e: gregex n m): uglang (gerase e) ≡ eval (fun _ => traces_tt) (fun _ => @lsyntax.e_var _) tsingle e.
proof: Proof. induction e; simpl gerase. apply lang_0. simpl. rewrite lsyntax.eval_var. reflexivity. reflexivity. now apply cup_weq. now apply dot_weq. now apply itr_weq. Qed.
imports: kat gregex ugregex ordinal positives glang