. intros hf
  cases hf with
  | inl hxs => apply mem_append_front _ _ _ hxs
  | inr hys => apply mem_append_back _ _ _ hys
case mp
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ∨ x ∈ ys → x ∈ xs ++ ys

case mpr
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys
case mpr
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys