proposition: Corollary kat_untype_weq n m (e f: gregex Pred src tgt n m): gerase e ≡ gerase f <-> e ≡ f.
proof: Proof. split. intro H. apply kat_complete_weq. rewrite 2untype_glang. now apply traces.restrict_weq. apply gerase_weq. Qed.
imports: boolean ugregex_dec kat_reification kat_untyping kat_completeness