exact h3
case h2
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
x : α
h1 : ∀ v ∈ ys, f v = g v
h2 : x ∈ xs
h3 : xs.length = ys.length
s1 : List.map f ys = List.map g ys
⊢ xs.length = ys.length
no goals