fact: Definition le_lift {m n : nat} (p : m <= n) (s : Success Toks Tok A m) : Success Toks Tok A n := let small := Nat.le_trans _ _ _ (small s) p in MkSuccess (value s) small (leftovers s).
imports: parseque(Indexed Sized) Coq(PeanoNat)