fact: Definition src' l := match l with | l_pos n _ | l_neg n _ => n | l_var i => s i end.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms