by
  intro State Op step undo inverse
  have failure : ∀ (ops : List Op), ops.foldl (fun prior op => prior.bind (step op)) none = none := by
    intro ops
    induction ops with
    | nil => rfl
    | cons op ops ih => simpa only [List.foldl_cons, Option.bind_none] using ih
  intro ops
  induction ops with
  | nil =>
    intro s t h
    simpa only [List.foldl_nil, List.reverse_nil] using h.symm
  | cons op ops ih =>
    intro s t h
    change ops.foldl (fun prior op => prior.bind (step op)) (step op s) = some t at h
    cases first : step op s with
    | none =>
      rw [first, failure] at h
      cases h
    | some mid =>
      have tail := ih mid t (by simpa only [first] using h)
      simp only [List.reverse_cons, List.foldl_append, List.foldl_cons, List.foldl_nil]
      rw [tail]
      exact inverse op s mid first