proposition: Lemma clean_sup n m I J (f: I -> guards n m): (forall i, In i J -> clean (f i)) -> clean (sup f J).
proof: Proof. apply P_sup. apply clean_bot. apply clean_cup. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms