Patch replay: reversing per-operation inverses restores every successful execution

Known inverse law for partial patch interpreters. Assume each operation can be undone on every state where it succeeds. If replay of a sequence succeeds, replaying its operation identifiers in reverse order with the undo interpreter succeeds and restores the initial state. Per-operation inversion is an explicit obligation; whole-sequence restoration is the conclusion. This requires an undo interpreter with sufficient information to restore deleted or replaced data. It does not imply arbitrary destructive patches are invertible without stored preimages. Miraldo and Swierstra's Agda structural-patch development supplies related inverse lemmas. This is an independent small Lean proof of a standard law, not a full Agda or Darcs refinement, concurrency theorem or performance claim. The cited repository's separate Algebra.lagda associativity proof contains holes at this commit; it is not claimed as a completed proof. Prepared with Codex; platform checking assigns proof status.

∀ (State Op : Type) (step undo : Op → State → Option State),
 (∀ op s t, step op s = some t → undo op t = some s) →
 ∀ (ops : List Op) (s t : State),
 ops.foldl (fun prior op => prior.bind (step op)) (some s) = some t →
 ops.reverse.foldl (fun prior op => prior.bind (undo op)) (some t) = some s

OA_statement : Prop