fact: Definition and (p : Parser Toks Tok M A n) (q : Box (Parser Toks Tok M B) n) : Parser Toks Tok M (A * B) n := andbind p (fun _ => q).
imports: Coq(PeanoNat) parseque(Category Induction Sized NEList Success EqDec)