proposition: Lemma teval_prd n (p: tst n): teval (g_prd' n p) ≡ inj p.
proof: Proof. unfold g_prd'. rewrite sup_map. unfold geval. setoid_rewrite <-inj_sup. apply inj_weq. symmetry. apply decomp_expr. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms