by
  have hAnyFalse : ∀ (α : Type) (xs : List α), xs.any (fun _ => false) = false := by
    intro α xs
    induction xs with
    | nil => rfl
    | cons a xs ih => simp [List.any_cons, ih]
  have hFilterFalse : ∀ (α : Type) (xs : List α), xs.filter (fun _ => false) = [] := by
    intro α xs
    induction xs with
    | nil => rfl
    | cons a xs ih => simp [ih]
  dsimp only [OA_statement]
  intro history finalState hValid hReplay event hMem
  by_cases hEmpty : event.2.1 = []
  · simp [hEmpty, hAnyFalse, hFilterFalse]
  · skip