fact: Definition gl n m (G: glang n m): lang := fun w => exists g, w = gword_to_word n g /\ proj1_sig G g.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms