proposition: Lemma teval_one n: teval (g_one' n) ≡ 1.
proof: Proof. unfold g_one'. rewrite teval_prd. apply inj_top. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms