fact: Definition v: forall n m, expr3 n m -> regex := eval (f':=fun _ => regex_tt) (fun l => r_var (lp l)).
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms