proposition: Lemma clean_elem_var a i b: clean1 (g_elem a (g_var i) b).
proof: Proof. unfold clean1, geval. rewrite 2G.lang_dot, 2G.lang_atom. setoid_rewrite atom_single_atom. rewrite gl_single'. rewrite 2eq_app_dot. do 2 setoid_rewrite R.lang_dot. setoid_rewrite R.lang_var. setoid_rewrite <- R_lang_atom. apply dotA. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms