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 α
hb : x ∈ reverseSpec xs
⊢ x ∈ xs
no goals