proposition: Lemma clean_single n m (g: guard n m): clean1 g -> clean [g].
proof: Proof. now intros ? ? [<-|[]]. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms