proposition: Lemma gword_tapp: forall x y z, tapp x y z -> forall n, gword_to_word n z = gword_to_word n x ++ gword_to_word' y.
proof: Proof. induction 1; simpl; intros n. now rewrite app_nil_r. reflexivity. now rewrite IHtapp, <-app_assoc. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms