ContT.ext

theorem ContT.ext : ∀ {r : Type u} {m : Type u → Type v} {α : Type w} {x y : ContT r m α}, (∀ (f : α → m r), x.run f = y.run f) → x = y

The theorem `ContT.ext` is a statement about equality in the context of continuation-passing style transformations. Specifically, it says that for any types `r`, `m`, and `α`, and any two values `x` and `y` of type `ContT r m α`, if for all functions `f` from `α` to `m r`, applying `f` to `x` and `y` via the `ContT.run` function yields the same result, then `x` and `y` must be equal. In other words, two continuation-passing style transformations are equal if they produce the same result when run with any continuation.

More concisely: If for all functions `f` from `α` to `m r`, the application of `f` to two values `x` and `y` in `ContT r m α` via `ContT.run` yields the same result, then `x` and `y` are equal.