Thunk.ext

theorem Thunk.ext : ∀ {α : Type u} {a b : Thunk α}, a.get = b.get → a = b

This theorem states that for any type `α` and any two elements `a` and `b` of the type `Thunk α`, if the result of the `Thunk.get` function applied to `a` equals the result of the `Thunk.get` function applied to `b`, then `a` equals `b`. In other words, two thunk objects are equal if and only if they produce the same value when their contained functions are invoked.

More concisely: For all types `α` and elements `a` and `b` of `Thunk α`, if `Thunk.get a = Thunk.get b`, then `a = b`.