proposition: Lemma clean_cup n m (e f: guards n m): clean e -> clean f -> clean (e++f).
proof: Proof. unfold clean. setoid_rewrite in_app_iff. intuition. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms