theorem Option.eq_of_eq_some {α : Type u} {x : Option α} {y : Option α} : (∀ (z : α), x = some z ↔ y = some z) → x = y

theorem Option.eq_none_of_isNone {α : Type u} {o : Option α} : Option.isNone o = true → o = none