The first-occurrence index fold

Pure transition and invariant shared by the direct list certificate and its legacy client.

def Turing.MultiTapeTM.Internal.ListIndex.idxStep {α : Type u_1} [DecidableEq α] (v : α) (s : Bool × ℕ) (a : α) : Bool × ℕ

Keep the first matching position, incrementing only while no match has appeared.

theorem Turing.MultiTapeTM.Internal.ListIndex.foldl_idxStep {α : Type u_1} [DecidableEq α] (v : α) (l : List α) (s : Bool × ℕ) : (List.foldl (idxStep v) s l).snd = s.snd + if s.fst = true then 0 else List.idxOf v l

The original first-occurrence fold returns the starting count plus the first index.