fact: Definition geval n m (x: guard n m) := match x with | @g_pred n a => g_atom n a | @g_elem n m a e b => g_atom n a ⋅ e ⋅ g_atom m b end.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms