proposition: Lemma gl_single' a i b: gl (tsingle' a i b) ≡ eq (atom_to_word (s i) a++[lp (l_var i)]++atom_to_word (t i) b).
proof: Proof. intro w; split. intros [g [-> <-]]. reflexivity. intros <-. eexists. split. 2: reflexivity. reflexivity. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms