proposition: Lemma o_level n m (e: gregex n m): e_level (o e) ≪ BKA.
proof: Proof. pose proof o_pred_level. induction e; simpl o; simpl e_level; rewrite ?merge_spec; intuition easy. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms