. intro hb
  cases hb with
  | inl h => rw [(mem_singleton_iff x y).mp h]; apply Mem.head
  | inr h => apply Mem.tail _ h
case mpr
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ [y] ∨ x ∈ ys → x ∈ y :: ys
no goals