fact: Definition nelist : Parser Toks Tok M A n -> Parser Toks Tok M (NEList A) n := Fix _ (fun _ rec p => map (uncurry consm) (andm p (Induction.app _ rec p))) _.
imports: Coq(PeanoNat) parseque(Category Induction Sized NEList Success EqDec)