proposition: Lemma empty_atom_dot n a b: a<>b -> g_atom n a ⋅ g_atom n b ≡ 0.
proof: Proof. intros. setoid_rewrite <-inj_cap. rewrite (empty_atom_cap H). apply inj_bot. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms