fact: Definition clean n m (e: guards n m) := forall g, In g e -> clean1 g.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms