cases O
α : Type u_1
x : α
O : Option α
⊢ some x ⊆ O ↔ some x = O
case none
α : Type u_1
x : α
⊢ some x ⊆ none ↔ some x = none

case some
α : Type u_1
x val✝ : α
⊢ some x ⊆ some val✝ ↔ some x = some val✝