proposition: Lemma clean_one' n: clean (g_one' n).
proof: Proof. apply clean_map. intros. apply clean_pred. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms