fact: Definition atom_to_word n (a: Atom) := map (fun i => if set.mem a i then lp (l_pos n i) else lp (l_neg n i)) (seq pred).
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms