no goals
α : Type u_1
β : Type u_2
γ : Type ?u.156112
δ : Type ?u.156115
σ : Type ?u.156118
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
p : α → β → Bool
hp : Primrec₂ p
a : β
l : List β
n : α
⊢ (bif p (id n) a then 0 else Nat.succ (List.findIdx (p n) l)) = List.findIdx (p n) (a :: l)
simp [List.findIdx_cons]