simp at h
case nil
α✝ : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
α : Type u
inst✝ : DecidableEq α
f : α → β
a : α
h : a ∈ []
⊢ lookup a (map (fun x => (x, f x)) []) = some (f a)
no goals