proposition: Lemma teval_var i: teval (g_var' i) ≡ g_var i.
proof: Proof. unfold g_var'. rewrite sup_sup. setoid_rewrite sup_sup. setoid_rewrite sup_singleton. unfold geval. setoid_rewrite <-dotxsum. setoid_rewrite <-dotA. rewrite <-dotsumx. setoid_rewrite sum_atoms. ra. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms