by
  dsimp only [OA_statement]
  intro actions position saved
  cases actions with
  | nil => cases saved <;> rfl
  | cons action rest =>
    rcases action with ⟨a, b⟩
    cases a <;> cases b
    · skip
    · skip
    · skip
    · cases saved <;> simp [List.takeWhile_cons]