proposition: Lemma o_pred_level x: e_level (o_pred x) ≪ BKA with o_npred_level x: e_level (o_npred x) ≪ BKA.
proof: Proof. destruct x; simpl o_pred; simpl e_level; rewrite ?merge_spec; intuition easy. destruct x; simpl o_npred; 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