The loops of the level parsers: stopping and running through a chain

theorem chain {α : Type} (loop : Nat → List Json → List Tok → Option α) (Q : List Tok → Prop)
    (W : Json × List Tok → Nat) (rest : List Tok) (hQr : Q rest) :
    ∀ (bs : List (Json × List Tok)), (∀ p ∈ bs, ∀ r, Q (p.2 ++ r)) →
      (∀ p ∈ bs, ∀ f acc r, Q r → W p ≤ f →
        loop (f + 1) acc (p.2 ++ r) = loop f (acc ++ [p.1]) r) →
      ∀ (acc : List Json) (f : Nat), (∀ p ∈ bs, W p + bs.length ≤ f) → bs.length ≤ f →
      loop f acc ((bs.flatMap Prod.snd) ++ rest) = loop (f - bs.length) (acc ++ bs.map Prod.fst) rest

A chain of blocks, each of which one loop step consumes (with fuel at least W of it).