proposition: Lemma wvo_uo n m (e: gregex n m): w (v (o e)) ≡ erase BKA (o e).
proof: Proof. apply wv_u, o_level. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms