proposition: Lemma R_lang_atom n a: R (v (o (g_atom n a))) ≡ latom n a.
proof: Proof. simpl o. unfold atom, atom_to_word. induction (seq pred). apply R.lang_1. simpl (sup _ _). setoid_rewrite R.lang_dot. setoid_rewrite (eq_app_dot _ [_]). apply dot_weq. case set.mem; apply R.lang_var. assumption. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms