proposition: Lemma gl_atom n a: gl (tatom n a) ≡ latom n a.
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