proposition: Lemma gl_nildot a n m (e: glang n m): exists e', gl (tatom n a ⋅ e) ≡ latom n a ⋅ e'.
proof: Proof. exists (fun w => exists g, proj1_sig e g /\ thead g = a /\ w = gword_to_word' g). rewrite weq_spec. split; intro w. intros [u [-> [? <- [v Hv H]]]]. apply tapp_nil_x_eq in H as [-> ->]. repeat eexists; eauto. apply gword_to_word_cut. intros [? <- [u (x&He&<-&->) ->]]. repeat eexists; eauto. apply eq_sym, gword_to_word_cut. apply tapp_nil_x. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms