theorem Thunk.ext_iff {α : Type u_1} {a : Thunk α} {b : Thunk α} : a = b ↔ a.get = b.get

theorem Thunk.ext {α : Type u_1} {a : Thunk α} {b : Thunk α} : a.get = b.get → a = b