{ simp[ha] at h; exact Or.inr ⟨ha, h⟩ }
case neg
α✝ : 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 a' : α
as : List α
ih : a ∈ as → lookup a (map (fun x => (x, f x)) as) = some (f a)
h : a = a' ∨ a ∈ as
ha : ¬a = a'
⊢ a = a' ∨ a ≠ a' ∧ a ∈ as
no goals