proposition: Lemma clean_pred n a: clean1 (@g_pred n a).
proof: Proof. unfold clean1, geval. rewrite G.lang_atom, R_lang_atom. apply gl_atom. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms