fact: Definition iterater {n : nat} (op : Parser Toks Tok M (A -> A) n) (val : Parser Toks Tok M A n) : Parser Toks Tok M A n := Fix _ (fun n rec op val => alt (iterater_aux n rec op val) val) n op val.
imports: Coq(PeanoNat) parseque(Category Induction Sized NEList Success EqDec)