. intro hb
  induction xs with
  | nil => contradiction
  | cons y ys ih =>
    simp only [reverseSpec] at hb
    rw [List.mem_append_comm] at hb
    simp only [HAppend.hAppend, Append.append, List.append] at hb
    cases hb with
    | head => exact Mem.head _
    | tail _ htail => exact Mem.tail _ (ih htail)
case mpr
α : Type u_1
x : α
xs : List α
⊢ x ∈ reverseSpec xs → x ∈ xs
no goals