fact: Definition fromView : View Toks Tok n -> Success Toks Tok Tok n := match n return View Toks Tok n -> Success Toks Tok Tok n with | O => False_rect _ | S n' => uncurry (fun t ts => MkSuccess t (Nat.le_refl _) ts) end.
imports: parseque(Indexed Sized) Coq(PeanoNat)