proposition: Lemma teval_dot n m p (x: guards n m) (y: guards m p): teval (g_dot' x y) ≡ teval x ⋅ teval y.
proof: Proof. unfold g_dot'. rewrite sup_sup. setoid_rewrite sup_sup. setoid_rewrite geval_dot. rewrite dotsumx. now setoid_rewrite dotxsum. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms