proposition: Lemma geval_fst n m (r: guard n m): geval r ≡ g_atom _ (fst r) ⋅ geval r.
proof: Proof. destruct r. simpl fst; unfold geval. now rewrite idem_atom_dot. simpl fst; unfold geval. now rewrite 2dotA, idem_atom_dot. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms