cases hb with
| head _ => apply Or.intro_left _ (List.Mem.head _)
| tail _ h' =>
  cases ys with
  | nil =>
    apply Or.intro_left
    apply List.Mem.tail
    simp at h'
    exact h'
  | cons y ys =>
    simp at h'
    cases ih h' with
    | inl hxxs =>
      apply Or.intro_left
      exact List.Mem.tail _ hxxs
    | inr hxys =>
      exact Or.intro_right _ hxys
case mpr.cons
α : Type u_1
x : α
ys : List α
z : α
xs : List α
ih : x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
hb : x ∈ z :: xs ++ ys
⊢ x ∈ z :: xs ∨ x ∈ ys
no goals