case _ c1 =>
  specialize h1 y a1
  contradiction
α β : 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
c1 : y = v
⊢ f y = a
no goals