proposition: Lemma clean_map n m I J (f: I -> guard n m): (forall i, In i J -> clean1 (f i)) -> clean (map f J).
proof: Proof. rewrite map_sup. intro. apply clean_sup. intros. apply clean_single. auto. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms