proposition: Lemma idem_atom_dot n a: g_atom n a ⋅ g_atom n a ≡ g_atom n a.
proof: Proof. setoid_rewrite <-inj_cap. now rewrite capI. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms