fact: Definition g_dot' n m p (h: guards n m) (k: guards m p) := \sup_(x\in h) \sup_(y\in k) g_dot1 x y.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms