exact this.of_eq <| fun a ps => by
  induction' ps with p ps <;> simp[List.lookup, *]
  cases ha : a == p.1 <;> simp[ha]
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
this✝ : Primrec₂ fun p q => bif p.1 == q.1.1 then some q.1.2 else q.2.2
this : Primrec₂ fun a l => List.recOn l none fun p x ih => bif a == p.1 then some p.2 else ih
⊢ Primrec₂ List.lookup
no goals