fact: Definition app (p : Parser Toks Tok M (A -> B) n) (q : Box (Parser Toks Tok M A) n) : Parser Toks Tok M B n := bind p (fun f => Induction.map (fun _ => map f) _ q).
imports: Coq(PeanoNat) parseque(Category Induction Sized NEList Success EqDec)