. intros hb
  induction xs with
  | nil => exact Or.intro_right _ hb
  | cons z xs ih =>
    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
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
no goals