fact: Definition ands (ps : NEList (Parser Toks Tok M A n)) : Parser Toks Tok M (NEList A) n := foldr1 (fun p ps => map (uncurry append) (and p ps)) (NEList.map (map singleton) ps).
imports: Coq(PeanoNat) parseque(Category Induction Sized NEList Success EqDec)