have : Primrec₂ (fun p q => bif p.1 == q.1.1 then q.1.2 else q.2.2 : α × List (α × β) → (α × β) × List (α × β) × Option β → Option β) :=
  cond (Primrec.beq.comp (fst.comp fst) (fst.comp $ fst.comp snd))
    (option_some.comp $ snd.comp $ fst.comp snd) (snd.comp $ snd.comp snd)
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
⊢ Primrec₂ List.lookup
α : 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
⊢ Primrec₂ List.lookup