proposition: Lemma typed_uglang_gerase n m (e: gregex n m): typed n m (uglang (gerase e)).
proof: Proof. induction e. intros [|] H. discriminate. destruct H. apply typed'_inj. apply typed'_single. revert IHe1 IHe2. apply typed'_cup. revert IHe1 IHe2. apply typed'_dot. revert IHe. apply typed'_itr. Qed.
imports: kat gregex ugregex ordinal positives glang