fact: Definition clean1 n m (e: guard n m) := gl (G (geval e)) ≡ R (v (o (geval e))).
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms