proposition: Lemma teval_str n (x: guards n n): teval (g_str' x) ≡ (teval x)^*.
proof: Proof. induction x as [|r q IH]; simpl g_str'. rewrite teval_one. symmetry. apply str0. simpl (sup _ _). setoid_rewrite (cupC (geval r)). rewrite str_pls. rewrite sup_app, teval_dot, teval_xitr, IH. rewrite (str_itr (_⋅_)). ra. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms