proposition: Theorem untype_glang n m (e: gregex n m): glang e ≡ restrict n m (uglang (gerase e)).
proof: Proof. symmetry. induction e. setoid_rewrite lang_0. apply restrict_0. setoid_rewrite restrict_inj. simpl. unfold ttraces_weq. simpl. now rewrite lsyntax.eval_var. apply restrict_single. etransitivity. 2: apply cup_weq; eassumption. apply restrict_pls. etransitivity. 2: apply dot_weq; eassumption. apply restrict_dot; apply typed_uglang_gerase. etransitivity. 2: apply itr_weq; eassumption. apply restrict_itr; apply typed_uglang_gerase. Qed.
imports: kat gregex ugregex ordinal positives glang