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