case _ c2 =>
  rfl
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
y : α
a1 : y ∈ ys
c2 : ¬y = v
⊢ f y = f y
no goals