induction' ps with p ps <;> simp[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
this : Primrec₂ fun a l => List.recOn l none fun p x ih => bif a == p.1 then some p.2 else ih
a : α
ps : List (α × β)
⊢ (List.recOn ps none fun p x ih => bif a == p.1 then some p.2 else ih) = List.lookup a ps
case cons
α : 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
a : α
p : α × β
ps : List (α × β)
tail_ih✝ : (List.recOn ps none fun p x ih => bif a == p.1 then some p.2 else ih) = List.lookup a ps
⊢ (bif a == p.1 then some p.2 else List.lookup a ps) =
    match a == p.1 with
    | true => some p.2
    | false => List.lookup a ps